• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
      • Aleobft-static
      • Aleobft-stake2
        • Correctness
        • Definition
          • Initialization
          • Transitions
          • States
            • Committees
              • Max-faulty-for-total
              • Bonded-committee-at-round
              • Committee-members-stake
              • Active-committee-at-round
              • 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
      • Aleobft-dynamic
      • 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
    • Riscv
    • 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-members-stake

Total stake of a set of members of the committee.

Signature

(committee-members-stake members commtt) → stake

Arguments

members — Guard (address-setp members).

commtt — Guard (committeep commtt).

Returns

stake — Type (natp stake).

We add up all the stakes of the members.

We prove various properties that relate this function to set operations.

The monotonicity property uses a (locally defined) custom induction, which removes from the second set the head of the first set in the recursive call, when the first set is not empty; this is needed to exclude the stake of that committee member (if present in the second set of committee members) in the induction hypothesis.

The union expansion properties is analogous to the property of cardinalities of sets, but with stake in this case. The total stake of the union of two sets is their sum, minus the stake of the intersection (if any), which the sum union counts twice.

Definitions and Theorems

Function: committee-members-stake

(defun committee-members-stake (members commtt)
  (declare (xargs :guard (and (address-setp members)
                              (committeep commtt))))
  (declare
       (xargs :guard (subset members (committee-members commtt))))
  (let ((__function__ 'committee-members-stake))
    (declare (ignorable __function__))
    (cond ((emptyp (address-set-fix members)) 0)
          (t (+ (committee-member-stake (address-fix (head members))
                                        commtt)
                (committee-members-stake (tail members)
                                         commtt))))))

Theorem: natp-of-committee-members-stake

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

Theorem: posp-of-committee-members-stake

(defthm posp-of-committee-members-stake
  (implies (not (emptyp (address-set-fix members)))
           (b* ((stake (committee-members-stake members commtt)))
             (posp stake)))
  :rule-classes (:rewrite :type-prescription))

Theorem: committee-members-stake-0-to-emptyp-members

(defthm committee-members-stake-0-to-emptyp-members
  (equal (equal (committee-members-stake members commtt)
                0)
         (emptyp (address-set-fix members))))

Theorem: committee-members-stake-when-emptyp-members

(defthm committee-members-stake-when-emptyp-members
  (implies (emptyp members)
           (equal (committee-members-stake members commtt)
                  0)))

Theorem: committee-members-stake-of-insert

(defthm committee-members-stake-of-insert
  (implies (and (addressp member)
                (address-setp members))
           (equal (committee-members-stake (insert member members)
                                           commtt)
                  (if (in member members)
                      (committee-members-stake members commtt)
                    (+ (committee-member-stake member commtt)
                       (committee-members-stake members commtt))))))

Theorem: committee-members-stake-of-delete

(defthm committee-members-stake-of-delete
  (implies (address-setp members)
           (equal (committee-members-stake (delete member members)
                                           commtt)
                  (if (in member members)
                      (- (committee-members-stake members commtt)
                         (committee-member-stake member commtt))
                    (committee-members-stake members commtt)))))

Theorem: committee-members-stake-monotone

(defthm committee-members-stake-monotone
  (implies (and (address-setp members1)
                (address-setp members2)
                (subset members1 members2))
           (<= (committee-members-stake members1 commtt)
               (committee-members-stake members2 commtt))))

Theorem: committee-members-stake-of-union

(defthm committee-members-stake-of-union
 (implies
    (and (address-setp members1)
         (address-setp members2))
    (equal (committee-members-stake (union members1 members2)
                                    commtt)
           (- (+ (committee-members-stake members1 commtt)
                 (committee-members-stake members2 commtt))
              (committee-members-stake (intersect members1 members2)
                                       commtt)))))

Theorem: committee-members-stake-of-intersect

(defthm committee-members-stake-of-intersect
  (implies
       (and (address-setp members1)
            (address-setp members2))
       (equal (committee-members-stake (intersect members1 members2)
                                       commtt)
              (- (+ (committee-members-stake members1 commtt)
                    (committee-members-stake members2 commtt))
                 (committee-members-stake (union members1 members2)
                                          commtt)))))

Theorem: committee-members-stake-of-difference

(defthm committee-members-stake-of-difference
 (implies
      (and (address-setp members1)
           (address-setp members2))
      (equal (committee-members-stake (difference members1 members2)
                                      commtt)
             (- (committee-members-stake (union members1 members2)
                                         commtt)
                (committee-members-stake members2 commtt)))))

Theorem: committee-members-stake-of-address-set-fix-members

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

Theorem: committee-members-stake-address-set-equiv-congruence-on-members

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

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

(defthm committee-members-stake-of-committee-fix-commtt
  (equal (committee-members-stake members (committee-fix commtt))
         (committee-members-stake members commtt)))

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

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