• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
      • Aleobft-static
      • Aleobft-dynamic
      • Aleobft-stake2
      • Aleobft-stake
        • Correctness
        • Definition
          • Initialization
          • Transitions
          • States
            • Committees
              • Max-faulty-for-total
              • Bonded-committee-at-round
              • Active-committee-at-round
              • Committee-members-stake
              • Update-committee-with-transaction
              • Committee-quorum-stake
              • Lookback
              • Committee-option
              • Update-committee-with-transaction-list
              • Committee-after-blocks
              • Same-bonded-committees-p
              • Same-active-committees-p
              • Committee
              • Committee-member-stake
              • Committee-total-stake
              • Committee-max-faulty-stake
              • Committee-nonemptyp
              • Committee-members
              • Address-pos-map
              • Genesis-committee
            • System-states
            • Certificates
            • Messages
            • Transactions
            • Validator-states
            • Addresses
            • Blocks
          • Events
      • 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) → commtt?

Arguments

round — Guard (posp round).

blocks — Guard (block-listp blocks).

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 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.

Among other properties, we prove that if a round has a bonded committeed, then every round before that round does as well. We also show that extending a blockchain does not affect the bonded committee at rounds that have a bonded committee calculable from the original blockchain.

Definitions and Theorems

Function: bonded-committee-at-round-loop

(defun bonded-committee-at-round-loop (round blocks)
  (declare (xargs :guard (and (posp round)
                              (block-listp blocks))))
  (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)))
      (bonded-committee-at-round-loop round (cdr blocks)))))

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)))
    (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)
                  (genesis-committee))))

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)
                  (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))
      (bonded-committee-at-round-loop round blocks))))

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)
         (bonded-committee-at-round-loop round blocks)))

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)
              (bonded-committee-at-round-loop round-equiv blocks)))
  :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))
      (bonded-committee-at-round-loop round blocks)))

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)
             (bonded-committee-at-round-loop round blocks-equiv)))
 :rule-classes :congruence)

Function: bonded-committee-at-round

(defun bonded-committee-at-round (round blocks)
  (declare (xargs :guard (and (posp round)
                              (block-listp blocks))))
  (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))))

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

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

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)))
             (implies commtt
                      (equal commtt (genesis-committee))))))

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)
                  (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))
    (equal (bonded-committee-at-round round (append blocks1 blocks))
           (bonded-committee-at-round round blocks))))

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)
                (< (pos-fix earlier) (pos-fix later)))
           (bonded-committee-at-round earlier blocks)))

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)
       (<= (pos-fix round)
           (+ 2 (blocks-last-round blocks)))))

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)
         (bonded-committee-at-round round blocks)))

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)
                  (bonded-committee-at-round round-equiv blocks)))
  :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))
         (bonded-committee-at-round round blocks)))

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)
                  (bonded-committee-at-round round blocks-equiv)))
  :rule-classes :congruence)