• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
      • Aleobft-static
        • Correctness
        • Definition
          • Transitions
          • Operations
            • Operations-author-round-pairs
            • Operations-certificate-retrieval
            • Operations-faults-and-quora
            • Operations-leaders
            • Operations-previous-certificates
            • Operations-dags
            • Operations-blockchain
            • Operations-voting
              • Tally-leader-votes
            • Operations-message-creation
          • States
          • Initialization
          • Events
      • Aleobft-dynamic
      • 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

• Operations-voting

Tally-leader-votes

Count the votes and non-votes for the leader.

Signature

(tally-leader-votes leader voters) → (mv yes-count no-count)

Arguments

leader — Guard (addressp leader).

voters — Guard (certificate-setp voters).

Returns

yes-count — Type (natp yes-count).

no-count — Type (natp no-count).

The leader input to this function is the address of the leader at some even round. The voters input to this function is the set of all certificates in the DAG in the immediately following odd round: these are all the voters for the leader. Each edge to the leader's certificate (in the preceding even round) counts as a `yes' vote, while its absence counts as a `no' vote. We return both counts.

Definitions and Theorems

Function: tally-leader-votes

(defun tally-leader-votes (leader voters)
  (declare (xargs :guard (and (addressp leader)
                              (certificate-setp voters))))
  (let ((__function__ 'tally-leader-votes))
    (declare (ignorable __function__))
    (b* (((when (emptyp voters)) (mv 0 0))
         (voter (head voters))
         ((mv yes-count no-count)
          (tally-leader-votes leader (tail voters))))
      (if (in leader (certificate->previous voter))
          (mv (1+ yes-count) no-count)
        (mv yes-count (1+ no-count))))))

Theorem: natp-of-tally-leader-votes.yes-count

(defthm natp-of-tally-leader-votes.yes-count
  (b* (((mv ?yes-count ?no-count)
        (tally-leader-votes leader voters)))
    (natp yes-count))
  :rule-classes :rewrite)

Theorem: natp-of-tally-leader-votes.no-count

(defthm natp-of-tally-leader-votes.no-count
  (b* (((mv ?yes-count ?no-count)
        (tally-leader-votes leader voters)))
    (natp no-count))
  :rule-classes :rewrite)

Theorem: tally-leader-votes-sum

(defthm tally-leader-votes-sum
  (b* (((mv ?yes-count ?no-count)
        (tally-leader-votes leader voters)))
    (equal (+ yes-count no-count)
           (cardinality voters))))

Theorem: tally-leader-votes-of-insert

(defthm tally-leader-votes-of-insert
 (equal (tally-leader-votes leader (insert voter voters))
        (if (in voter voters)
            (tally-leader-votes leader voters)
          (mv (if (in leader (certificate->previous voter))
                  (1+ (mv-nth 0 (tally-leader-votes leader voters)))
                (mv-nth 0 (tally-leader-votes leader voters)))
              (if (not (in leader (certificate->previous voter)))
                  (1+ (mv-nth 1 (tally-leader-votes leader voters)))
                (mv-nth 1
                        (tally-leader-votes leader voters)))))))