• 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

Active-committee-at-round

Active committee at a given round.

Signature

(active-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?).

As explained in lookback, the active committee for a given round, i.e. the one in charge of the round, is the one bonded at the earlier round whose distance is B from the round of interest, or the genesis committee if such earlier round does not exist (i.e. it would be 0 or negative, before round 1). This ACL2 function formalizes this notion of active committee.

Note that there is no guarantee that there is a bonded committee at round R - B, where R is the round of interest. Thus, this function returns an optional committee, nil if no committee is available.

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 bonded-committee-at-round.

Definitions and Theorems

Function: active-committee-at-round

(defun active-committee-at-round (round blocks all-vals)
  (declare (xargs :guard (and (posp round)
                              (block-listp blocks)
                              (address-setp all-vals))))
  (let ((__function__ 'active-committee-at-round))
    (declare (ignorable __function__))
    (if (> (pos-fix round) (lookback))
        (bonded-committee-at-round (- (pos-fix round) (lookback))
                                   blocks all-vals)
      (genesis-committee))))

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

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

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

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

Theorem: active-committee-at-previous-round-when-at-round

(defthm active-committee-at-previous-round-when-at-round
  (implies (and (active-committee-at-round round blocks all-vals)
                (> (pos-fix round) 1))
           (active-committee-at-round (1- round)
                                      blocks all-vals)))

Theorem: active-committee-at-previous2-round-when-at-round

(defthm active-committee-at-previous2-round-when-at-round
  (implies (and (active-committee-at-round round blocks all-vals)
                (> (pos-fix round) 2))
           (active-committee-at-round (- round 2)
                                      blocks all-vals)))

Theorem: active-committee-at-previous3-round-when-at-round

(defthm active-committee-at-previous3-round-when-at-round
  (implies (and (active-committee-at-round round blocks all-vals)
                (> (pos-fix round) 3))
           (active-committee-at-round (- round 3)
                                      blocks all-vals)))

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

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

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

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

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

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

Theorem: active-committee-at-round-of-round-leq-2+lookback

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

Theorem: active-committee-at-round-of-append

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

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

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

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

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

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

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

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

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

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

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

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

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