		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 all-vals) → new-commtt
Arguments: trans — Guard (transactionp trans).; commtt — Guard (committeep commtt).; all-vals — Guard (address-setp all-vals).
Returns: new-commtt — Type (committeep new-commtt).

There are three kinds of transactions: bonding, unbonding, and other. A bonding transaction adds the validator address to the committee; there is no change if the validator is already in the committee. An unbonding transaction removes the validator address from the committee (except in a case explained below); there is no change if the validator is not in the committee. The other kind of transaction leaves the committee unchanged.

In order to maintain the non-emptiness of the committee, attempting to remove the only member of the committee does not actually remove it. An implementation of AleoBFT may require larger minimal committees, but for the purposes of our model, it suffices for the committee to be never empty. The protocol works, although in a degenerate way, with just one validator.

It is an interesting question whether an AleoBFT implementation should have mechanisms in place to guarantee minimal committee sizes. If it does, our model of unbonding captures a form of that. 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. If that is the case, our model of unbonding is still adequate to capture the situation in which the whole network has not failed; as mentioned above, the unbonding transaction that does not unbond can be simply regarded as if it were an :other kind of transaction.

In order to maintain the fact that the committee is a subset of all the validators in the system, we pass to this function an input all-vals that consists of the set of all validator addresses in the system. If a bonding transaction references an address outside that set, the committee is unchanged by that transaction, i.e. it is ignored. This is just a technical device in our formal model; it does not mean that validators need to know all-vals in order to calculate committees. In an AleoBFT implementation, the existence of a bonding transaction with a certain address means that a validator with that address is part of the system, which in our model consists of all possible validators, and the one with that address is certainly a possibly validator. Thus, this is more of a constraint on the system of all validators than on the calculation of committees per se.

We prove that, if the old committee's members are in all-vals, then the same holds for the new committee's members. That is, the invariant is maintained.

Definitions and Theorems

Function: update-committee-with-transaction

(defun update-committee-with-transaction (trans commtt all-vals)
  (declare (xargs :guard (and (transactionp trans)
                              (committeep commtt)
                              (address-setp all-vals))))
  (let ((__function__ 'update-committee-with-transaction))
    (declare (ignorable __function__))
    (transaction-case
         trans :bond
         (b* ((addresses (committee->addresses commtt))
              (new-addresses (insert trans.validator addresses)))
           (if (in trans.validator
                   (address-set-fix all-vals))
               (change-committee commtt
                                 :addresses new-addresses)
             (committee-fix commtt)))
         :unbond
         (b* ((addresses (committee->addresses commtt))
              (new-addresses (delete trans.validator addresses)))
           (if (emptyp new-addresses)
               (committee-fix commtt)
             (change-committee commtt
                               :addresses new-addresses)))
         :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 all-vals)))
   (committeep new-commtt))
  :rule-classes :rewrite)

Theorem: update-committee-with-transactions-subset-all-vals

(defthm update-committee-with-transactions-subset-all-vals
 (implies
  (and (address-setp all-vals)
       (subset (committee-members commtt)
               all-vals))
  (b*
   ((?new-commtt
         (update-committee-with-transaction trans commtt all-vals)))
   (subset (committee-members new-commtt)
           all-vals))))

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 all-vals)
         (update-committee-with-transaction trans commtt all-vals)))

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 all-vals)
   (update-committee-with-transaction trans-equiv commtt all-vals)))
 :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)
                                        all-vals)
     (update-committee-with-transaction trans commtt all-vals)))

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 all-vals)
   (update-committee-with-transaction trans commtt-equiv all-vals)))
 :rule-classes :congruence)

Theorem: update-committee-with-transaction-of-address-set-fix-all-vals

(defthm
      update-committee-with-transaction-of-address-set-fix-all-vals
  (equal (update-committee-with-transaction
              trans commtt (address-set-fix all-vals))
         (update-committee-with-transaction trans commtt all-vals)))

Theorem: update-committee-with-transaction-address-set-equiv-congruence-on-all-vals

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