		Search-engine friendly clone of the ACL2 documentation.

Committees

Update-committee-with-transaction

Update a committee with a transaction.

Signature
(update-committee-with-transaction trans commtt) → new-commtt
Arguments: trans — Guard (transactionp trans).; commtt — Guard (committeep commtt).
Returns: new-commtt — Type (committeep new-commtt).

There are three kinds of transactions: bonding, unbonding, and other. A bonding transaction has a different effect depending on whether the validator is already in the committee or not: if it is not already in the committee, it is added to the committee, with associated the stake indicated in the transaction; if the validator is already in the committee, its associated stake is increased by the amount indicated in the transaction. An unbonding transaction removes the validator from the committee, along with its stake; there is no change if the validator is not in the committee. The other kind of transaction leaves the committee unchanged.

It is an interesting question whether an AleoBFT implementation should have mechanisms in place to guarantee minimal committee sizes. If it does not, which is plausible since validators should be generally free to bond and unbond as they want, then the whole network could be considered to fail if all validators unbond and there is nobody to run the network.

Definitions and Theorems

Function: update-committee-with-transaction

(defun update-committee-with-transaction (trans commtt)
 (declare (xargs :guard (and (transactionp trans)
                             (committeep commtt))))
 (let ((__function__ 'update-committee-with-transaction))
  (declare (ignorable __function__))
  (transaction-case
   trans :bond
   (b*
    ((members-with-stake (committee->members-with-stake commtt))
     (member-with-stake
          (omap::assoc trans.validator members-with-stake))
     (new-stake
       (if member-with-stake (+ trans.stake (cdr member-with-stake))
         trans.stake))
     (new-members-with-stake
          (omap::update trans.validator
                        new-stake members-with-stake)))
    (committee new-members-with-stake))
   :unbond
   (b* ((members-with-stake (committee->members-with-stake commtt))
        (new-members-with-stake
             (omap::delete trans.validator members-with-stake)))
     (committee new-members-with-stake))
   :other (committee-fix commtt))))

Theorem: committeep-of-update-committee-with-transaction

(defthm committeep-of-update-committee-with-transaction
 (b* ((new-commtt (update-committee-with-transaction trans commtt)))
   (committeep new-commtt))
 :rule-classes :rewrite)

Theorem: update-committee-with-transaction-of-transaction-fix-trans

(defthm update-committee-with-transaction-of-transaction-fix-trans
  (equal (update-committee-with-transaction (transaction-fix trans)
                                            commtt)
         (update-committee-with-transaction trans commtt)))

Theorem: update-committee-with-transaction-transaction-equiv-congruence-on-trans

(defthm
 update-committee-with-transaction-transaction-equiv-congruence-on-trans
 (implies
     (transaction-equiv trans trans-equiv)
     (equal (update-committee-with-transaction trans commtt)
            (update-committee-with-transaction trans-equiv commtt)))
 :rule-classes :congruence)

Theorem: update-committee-with-transaction-of-committee-fix-commtt

(defthm update-committee-with-transaction-of-committee-fix-commtt
 (equal
    (update-committee-with-transaction trans (committee-fix commtt))
    (update-committee-with-transaction trans commtt)))

Theorem: update-committee-with-transaction-committee-equiv-congruence-on-commtt

(defthm
 update-committee-with-transaction-committee-equiv-congruence-on-commtt
 (implies
     (committee-equiv commtt commtt-equiv)
     (equal (update-committee-with-transaction trans commtt)
            (update-committee-with-transaction trans commtt-equiv)))
 :rule-classes :congruence)