• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
      • Aleobft-static
      • Aleobft-dynamic
        • Correctness
        • Definition
          • Initialization
          • Transitions
          • States
            • Committees
              • Update-committee-with-transaction
              • Max-faulty-for-total
              • Bonded-committee-at-round
              • Active-committee-at-round
              • Update-committee-with-transaction-list
              • Committee-after-blocks
              • Lookback
              • Committee-quorum
              • Committee-option
              • Committee
              • Committee-members
              • Committee-total
              • Committee-max-faulty
              • Same-bonded-committees-p
              • Same-active-committees-p
              • Genesis-committee
            • System-states
            • Certificates
            • Messages
            • Transactions
            • Validator-states
            • Addresses
            • Blocks
          • Events
      • Aleobft-stake2
      • Aleobft-stake
      • Library-extensions
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Committees

Bonded-committee-at-round

Bonded committee at a given round.

Signature

(bonded-committee-at-round round blocks all-vals) → commtt?

Arguments

round — Guard (posp round).

blocks — Guard (block-listp blocks).

all-vals — Guard (address-setp all-vals).

Returns

commtt? — Type (committee-optionp commtt?).

This is the committee that results from updating the genesis committee with all the transactions up to the latest block not after the round. The previous sentence is approximate, so we need to clarify it. First, the bonded committee at round 1 is certainly the genesis committee. If there is a block at round 2, with transactions that change the committee, we have two choices for the bonded committee at round 2: it could be still the genesis committee, or it could be the new committee after the block; this depends on whether we consider the new committee to be bonded at the beginning or at the end of round 2. The same kind of choice applies to any other even round with a block that changes the committee; on the other hand, it is always clear what the bonded committee at an odd round is, and also at even rounds without blocks or with blocks that do not change the committee.

There seems to be no real criterion to choose between the two options, and it should no matter to correctness, i.e. the protocol should be correct either way. We choose to change committee at the end of the even round. Thus, the bonded committee at round 2 is always the genesis committee, which may change in round 3.

This ACL2 function returns the committee bonded at a given round, according to the choice explained above, But note that not every round has a bonded committee: after a certain round, the bonded committee is unknown, because there are no blocks yet. Suppose that the last block is at (even) round R. Then we know the committee bonded at rounds R+1 and R+2, namely the committee resulting from all the transactions in the blockchain. We also know the committee bonded at R and earlier rounds, based on prefixes of the full blockchain. But we do not know the committee bounded at rounds R+3 and later, because a block may be committed at round R+2, which would then apply to R+3. This is why this ACL2 function returns an optional committee, which is nil if the committee is not known.

The above also works if we take R = 0, which is not a round number because round numbers are positive, but it can be regarded as somewhat of a pseudo-round number. If the blockchain is empty, we know the bonded committee at rounds 1 and 2, namely the genesis committee; but we do not know the bonded committee at round 3 and later, because a block may be committed at round 2 which determines a new bonded committee at round 3 (and 4).

So here is how this ACL2 function to calculate the bonded committee works. First, we calculate the latest round L for which we have a block, or 0 if the blockchain is empty. If the requested round (i.e. the round input of this function) is more than 2 rounds later than L, then the bonded committee is unknown, and we return nil. Recall that, as explained in validator-state, the latest block is the leftmost, i.e. the car. If instead the requested round is less than or equal to L+2, then it has a bonded committee, which we calculate in a loop.

Since, as explained above, we regard the committe as changing at the end of the even round of each block, we need to find the latest block whose round is below round. Assuming that the block rounds are ordered (more on this later), we stop the loop as soon as we find a block with round below round: we calculate the committee from that block and preceding blocks, and we return that as the bonded committee. If we reach the end of the blockchain, we return the genesis committee.

In a well-formed blockchain, the blocks all have even rounds, and the rounds strictly decrease going from left to right in the list. In this function we do not have this invariant, but we do not need that in order to define this function. Note that the loop terminates regardless of the round numbers. But in order to understand this function, it is best to think of the blocks input forming a well-formed blockchain.

The role of the all-vals input is explained in update-committee-with-transaction.

We show that the bonded committee, if calculable, has members in all-vals, so long as the genesis committee does. This derives from the analogous property of committee-after-blocks.

Definitions and Theorems

Function: bonded-committee-at-round-loop

(defun bonded-committee-at-round-loop (round blocks all-vals)
  (declare (xargs :guard (and (posp round)
                              (block-listp blocks)
                              (address-setp all-vals))))
  (let ((__function__ 'bonded-committee-at-round-loop))
    (declare (ignorable __function__))
    (b* (((when (endp blocks))
          (genesis-committee))
         ((when (> (pos-fix round)
                   (block->round (car blocks))))
          (committee-after-blocks blocks all-vals)))
      (bonded-committee-at-round-loop round (cdr blocks)
                                      all-vals))))

Theorem: committeep-of-bonded-committee-at-round-loop

(defthm committeep-of-bonded-committee-at-round-loop
  (b*
   ((commtt (bonded-committee-at-round-loop round blocks all-vals)))
   (committeep commtt))
  :rule-classes :rewrite)

Theorem: bonded-committee-at-round-loop-when-no-blocks

(defthm bonded-committee-at-round-loop-when-no-blocks
  (implies
       (endp blocks)
       (equal (bonded-committee-at-round-loop round blocks all-vals)
              (genesis-committee))))

Theorem: bonded-committee-at-round-loop-subset-all-vals

(defthm bonded-committee-at-round-loop-subset-all-vals
 (implies
  (and (address-setp all-vals)
       (subset (committee-members (genesis-committee))
               all-vals))
  (b* ((?commtt
            (bonded-committee-at-round-loop round blocks all-vals)))
    (subset (committee-members commtt)
            all-vals))))

Theorem: bonded-committee-at-round-loop-of-round-leq-2

(defthm bonded-committee-at-round-loop-of-round-leq-2
  (implies
       (and (blocks-ordered-even-p blocks)
            (<= (pos-fix round) 2))
       (equal (bonded-committee-at-round-loop round blocks all-vals)
              (genesis-committee))))

Theorem: bonded-committee-at-round-loop-of-append-no-change

(defthm bonded-committee-at-round-loop-of-append-no-change
 (implies
  (and (blocks-ordered-even-p (append blocks1 blocks))
       (or (endp blocks1)
           (<= (pos-fix round)
               (block->round (car (last blocks1))))))
  (equal
       (bonded-committee-at-round-loop round (append blocks1 blocks)
                                       all-vals)
       (bonded-committee-at-round-loop round blocks all-vals))))

Theorem: bonded-committee-at-round-loop-of-pos-fix-round

(defthm bonded-committee-at-round-loop-of-pos-fix-round
  (equal (bonded-committee-at-round-loop (pos-fix round)
                                         blocks all-vals)
         (bonded-committee-at-round-loop round blocks all-vals)))

Theorem: bonded-committee-at-round-loop-pos-equiv-congruence-on-round

(defthm bonded-committee-at-round-loop-pos-equiv-congruence-on-round
 (implies
  (acl2::pos-equiv round round-equiv)
  (equal
      (bonded-committee-at-round-loop round blocks all-vals)
      (bonded-committee-at-round-loop round-equiv blocks all-vals)))
 :rule-classes :congruence)

Theorem: bonded-committee-at-round-loop-of-block-list-fix-blocks

(defthm bonded-committee-at-round-loop-of-block-list-fix-blocks
  (equal
       (bonded-committee-at-round-loop round (block-list-fix blocks)
                                       all-vals)
       (bonded-committee-at-round-loop round blocks all-vals)))

Theorem: bonded-committee-at-round-loop-block-list-equiv-congruence-on-blocks

(defthm
 bonded-committee-at-round-loop-block-list-equiv-congruence-on-blocks
 (implies
  (block-list-equiv blocks blocks-equiv)
  (equal
      (bonded-committee-at-round-loop round blocks all-vals)
      (bonded-committee-at-round-loop round blocks-equiv all-vals)))
 :rule-classes :congruence)

Theorem: bonded-committee-at-round-loop-of-address-set-fix-all-vals

(defthm bonded-committee-at-round-loop-of-address-set-fix-all-vals
  (equal (bonded-committee-at-round-loop
              round blocks (address-set-fix all-vals))
         (bonded-committee-at-round-loop round blocks all-vals)))

Theorem: bonded-committee-at-round-loop-address-set-equiv-congruence-on-all-vals

(defthm
 bonded-committee-at-round-loop-address-set-equiv-congruence-on-all-vals
 (implies
  (address-set-equiv all-vals all-vals-equiv)
  (equal
      (bonded-committee-at-round-loop round blocks all-vals)
      (bonded-committee-at-round-loop round blocks all-vals-equiv)))
 :rule-classes :congruence)

Function: bonded-committee-at-round

(defun bonded-committee-at-round (round blocks all-vals)
  (declare (xargs :guard (and (posp round)
                              (block-listp blocks)
                              (address-setp all-vals))))
  (let ((__function__ 'bonded-committee-at-round))
    (declare (ignorable __function__))
    (b* (((when (> (pos-fix round)
                   (+ 2 (blocks-last-round blocks))))
          nil))
      (bonded-committee-at-round-loop round blocks all-vals))))

Theorem: committee-optionp-of-bonded-committee-at-round

(defthm committee-optionp-of-bonded-committee-at-round
  (b* ((commtt? (bonded-committee-at-round round blocks all-vals)))
    (committee-optionp commtt?))
  :rule-classes :rewrite)

Theorem: bonded-committee-at-earlier-round-when-at-later-round

(defthm bonded-committee-at-earlier-round-when-at-later-round
  (implies (and (bonded-committee-at-round later blocks all-vals)
                (< (pos-fix earlier) (pos-fix later)))
           (bonded-committee-at-round earlier blocks all-vals)))

Theorem: bonded-committee-at-round-when-no-blocks

(defthm bonded-committee-at-round-when-no-blocks
 (implies
    (endp blocks)
    (b* ((commtt (bonded-committee-at-round round blocks all-vals)))
      (implies commtt
               (equal commtt (genesis-committee))))))

Theorem: bonded-committee-at-round-subset-all-vals

(defthm bonded-committee-at-round-subset-all-vals
 (implies
  (and (address-setp all-vals)
       (subset (committee-members (genesis-committee))
               all-vals))
  (b* ((?commtt? (bonded-committee-at-round round blocks all-vals)))
    (implies commtt?
             (subset (committee-members commtt?)
                     all-vals)))))

Theorem: bonded-committee-at-round-iff-round-upper-bound

(defthm bonded-committee-at-round-iff-round-upper-bound
  (iff (bonded-committee-at-round round blocks all-vals)
       (<= (pos-fix round)
           (+ 2 (blocks-last-round blocks)))))

Theorem: bonded-committee-at-round-of-round-leq-2

(defthm bonded-committee-at-round-of-round-leq-2
  (implies (and (blocks-ordered-even-p blocks)
                (<= (pos-fix round) 2))
           (equal (bonded-committee-at-round round blocks all-vals)
                  (genesis-committee))))

Theorem: bonded-committee-at-round-of-append-no-change

(defthm bonded-committee-at-round-of-append-no-change
 (implies
     (and (blocks-ordered-even-p (append blocks1 blocks))
          (bonded-committee-at-round round blocks all-vals))
     (equal (bonded-committee-at-round round (append blocks1 blocks)
                                       all-vals)
            (bonded-committee-at-round round blocks all-vals))))

Theorem: bonded-committee-at-round-of-pos-fix-round

(defthm bonded-committee-at-round-of-pos-fix-round
  (equal (bonded-committee-at-round (pos-fix round)
                                    blocks all-vals)
         (bonded-committee-at-round round blocks all-vals)))

Theorem: bonded-committee-at-round-pos-equiv-congruence-on-round

(defthm bonded-committee-at-round-pos-equiv-congruence-on-round
 (implies
    (acl2::pos-equiv round round-equiv)
    (equal (bonded-committee-at-round round blocks all-vals)
           (bonded-committee-at-round round-equiv blocks all-vals)))
 :rule-classes :congruence)

Theorem: bonded-committee-at-round-of-block-list-fix-blocks

(defthm bonded-committee-at-round-of-block-list-fix-blocks
  (equal (bonded-committee-at-round round (block-list-fix blocks)
                                    all-vals)
         (bonded-committee-at-round round blocks all-vals)))

Theorem: bonded-committee-at-round-block-list-equiv-congruence-on-blocks

(defthm
    bonded-committee-at-round-block-list-equiv-congruence-on-blocks
 (implies
    (block-list-equiv blocks blocks-equiv)
    (equal (bonded-committee-at-round round blocks all-vals)
           (bonded-committee-at-round round blocks-equiv all-vals)))
 :rule-classes :congruence)

Theorem: bonded-committee-at-round-of-address-set-fix-all-vals

(defthm bonded-committee-at-round-of-address-set-fix-all-vals
  (equal (bonded-committee-at-round
              round blocks (address-set-fix all-vals))
         (bonded-committee-at-round round blocks all-vals)))

Theorem: bonded-committee-at-round-address-set-equiv-congruence-on-all-vals

(defthm
 bonded-committee-at-round-address-set-equiv-congruence-on-all-vals
 (implies
    (address-set-equiv all-vals all-vals-equiv)
    (equal (bonded-committee-at-round round blocks all-vals)
           (bonded-committee-at-round round blocks all-vals-equiv)))
 :rule-classes :congruence)