• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Riscv
      • Taspi
      • Bitcoin
      • 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
      • Axe
      • Aleo
        • Aleobft
          • Correctness
            • Unequivocal-dags-def-and-init
            • Same-committees-def-and-implied
            • Dag-omni-paths
            • Signer-records
            • Unequivocal-dags-next
            • Quorum-intersection
            • Dag-previous-quorum-def-and-init-and-next
            • Unequivocal-signed-certificates
            • Signed-previous-quorum
              • Signed-previous-quorum-p-of-next
              • Validator-signed-previous-quorum-p
                • Signed-previous-quorum-p
                • Signed-previous-quorum-p-when-init
                • Signed-previous-quorum-p-of-events-next
                • Signed-previous-quorum-p-when-reachable
              • Nonforking-anchors-def-and-init-and-next
              • Successor-predecessor-intersection
              • Fault-tolerance
              • Last-anchor-voters-def-and-init-and-next
              • Signer-quorum
              • Committed-redundant-def-and-init-and-next
              • Nonforking-blockchains-def-and-init
              • Blockchain-redundant-def-and-init-and-next
              • No-self-endorsed
              • Last-anchor-present
              • Anchors-extension
              • Nonforking-blockchains-next
              • Backward-closure
              • Last-blockchain-round
              • Dag-certificate-next
              • Omni-paths-def-and-implied
              • Ordered-blockchain
              • Simultaneous-induction
              • System-certificates
              • Last-anchor-def-and-init
              • Last-anchor-next
              • Dag-previous-quorum
              • Signed-certificates
              • Committed-anchor-sequences
              • Omni-paths
              • Last-anchor-voters
              • Unequivocal-dags
              • Nonforking-blockchains
              • Nonforking-anchors
              • Committed-redundant
              • Same-committees
              • Blockchain-redundant
            • Definition
            • Library-extensions
          • Aleovm
          • Leo
        • Bigmems
        • Builtins
        • Execloader
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Community
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Signed-previous-quorum

    Validator-signed-previous-quorum-p

    Check if either a certificate has round 1 and it has no references to previous certificates, or the round is not 1 and the certificate's references to previous certificates are in the committee for the round just before the certificate round and form a non-zero quorum in that committee, where the committee is calculated by a validator (represented by its state).

    Signature
    (validator-signed-previous-quorum-p cert vstate) → yes/no
    Arguments
    cert — Guard (certificatep cert).
    vstate — Guard (validator-statep vstate).
    Returns
    yes/no — Type (booleanp yes/no).

    This is used by signed-previous-quorum-p to define our invariant. The validator whose state is vstate is the one that has signed the certificate. The guard ensures that the validator can calculate the committee.

    The validator must be able to calculate the committee; this is part of the invariant definition. To check the non-zeroness of the quorum, we equivalently check the non-emptiness of the previous references.

    Definitions and Theorems

    Function: validator-signed-previous-quorum-p

    (defun validator-signed-previous-quorum-p (cert vstate)
     (declare (xargs :guard (and (certificatep cert)
                                 (validator-statep vstate))))
     (let ((__function__ 'validator-signed-previous-quorum-p))
      (declare (ignorable __function__))
      (b* (((validator-state vstate) vstate)
           ((certificate cert) cert))
       (if (= (certificate->round cert) 1)
           (emptyp (certificate->previous cert))
        (b*
         ((commtt
               (active-committee-at-round (1- (certificate->round cert))
                                          vstate.blockchain)))
         (and commtt
              (not (emptyp (certificate->previous cert)))
              (subset (certificate->previous cert)
                      (committee-members commtt))
              (>= (committee-members-stake (certificate->previous cert)
                                           commtt)
                  (committee-quorum-stake commtt))))))))

    Theorem: booleanp-of-validator-signed-previous-quorum-p

    (defthm booleanp-of-validator-signed-previous-quorum-p
      (b* ((yes/no (validator-signed-previous-quorum-p cert vstate)))
        (booleanp yes/no))
      :rule-classes :rewrite)

    Theorem: validator-signed-previous-quorum-p-of-certificate-fix-cert

    (defthm validator-signed-previous-quorum-p-of-certificate-fix-cert
      (equal (validator-signed-previous-quorum-p (certificate-fix cert)
                                                 vstate)
             (validator-signed-previous-quorum-p cert vstate)))

    Theorem: validator-signed-previous-quorum-p-certificate-equiv-congruence-on-cert

    (defthm
     validator-signed-previous-quorum-p-certificate-equiv-congruence-on-cert
     (implies
         (certificate-equiv cert cert-equiv)
         (equal (validator-signed-previous-quorum-p cert vstate)
                (validator-signed-previous-quorum-p cert-equiv vstate)))
     :rule-classes :congruence)

    Theorem: validator-signed-previous-quorum-p-of-validator-state-fix-vstate

    (defthm
       validator-signed-previous-quorum-p-of-validator-state-fix-vstate
      (equal (validator-signed-previous-quorum-p
                  cert (validator-state-fix vstate))
             (validator-signed-previous-quorum-p cert vstate)))

    Theorem: validator-signed-previous-quorum-p-validator-state-equiv-congruence-on-vstate

    (defthm
     validator-signed-previous-quorum-p-validator-state-equiv-congruence-on-vstate
     (implies
         (validator-state-equiv vstate vstate-equiv)
         (equal (validator-signed-previous-quorum-p cert vstate)
                (validator-signed-previous-quorum-p cert vstate-equiv)))
     :rule-classes :congruence)