• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Aleobft
      • Aleobft-static
      • Aleobft-stake2
      • Aleobft-dynamic
      • Aleobft-stake
      • Aleobft-proposals
        • 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-validators-stake
              • Committee-after-blocks
              • Same-bonded-committees-p
              • Same-active-committees-p
              • Committee-validator-stake
              • Committee
              • Committee-member-stake
              • Committee-total-stake
              • Committee-max-faulty-stake
              • Committee-nonemptyp
              • Committee-members
              • Address-pos-map
              • Genesis-committee
            • System-states
            • Certificates
            • Transactions
            • Messages
            • Proposals
            • Validator-states
            • Addresses
            • Blocks
          • Events
          • Reachability
        • Correctness
      • Library-extensions
    • Acre
    • Milawa
    • Smtlink
    • 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
    • Riscv
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • 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

Committee-validators-stake

Total stake of a set of validators with respect to a committee.

Signature

(committee-validators-stake vals commtt) → stake

Arguments

vals — Guard (address-setp vals).

commtt — Guard (committeep commtt).

Returns

stake — Type (natp stake).

The validators may or may not be members of the committee. We add up the stake of the validators who are members, while the validators who are not members contribute 0 stake.

Definitions and Theorems

Function: committee-validators-stake

(defun committee-validators-stake (vals commtt)
  (declare (xargs :guard (and (address-setp vals)
                              (committeep commtt))))
  (let ((__function__ 'committee-validators-stake))
    (declare (ignorable __function__))
    (committee-members-stake (intersect (address-set-fix vals)
                                        (committee-members commtt))
                             commtt)))

Theorem: natp-of-committee-validators-stake

(defthm natp-of-committee-validators-stake
  (b* ((stake (committee-validators-stake vals commtt)))
    (natp stake))
  :rule-classes :rewrite)

Theorem: committee-validators-stake-of-address-set-fix-vals

(defthm committee-validators-stake-of-address-set-fix-vals
  (equal (committee-validators-stake (address-set-fix vals)
                                     commtt)
         (committee-validators-stake vals commtt)))

Theorem: committee-validators-stake-address-set-equiv-congruence-on-vals

(defthm
    committee-validators-stake-address-set-equiv-congruence-on-vals
  (implies (address-set-equiv vals vals-equiv)
           (equal (committee-validators-stake vals commtt)
                  (committee-validators-stake vals-equiv commtt)))
  :rule-classes :congruence)

Theorem: committee-validators-stake-of-committee-fix-commtt

(defthm committee-validators-stake-of-committee-fix-commtt
  (equal (committee-validators-stake vals (committee-fix commtt))
         (committee-validators-stake vals commtt)))

Theorem: committee-validators-stake-committee-equiv-congruence-on-commtt

(defthm
    committee-validators-stake-committee-equiv-congruence-on-commtt
  (implies (committee-equiv commtt commtt-equiv)
           (equal (committee-validators-stake vals commtt)
                  (committee-validators-stake vals commtt-equiv)))
  :rule-classes :congruence)