• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Pfcs
    • Wp-gen
    • Dimacs-reader
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Riscv
    • 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
        • Definition
          • Initialization
          • Transitions
          • States
            • Committees
            • System-states
            • Certificates
            • Messages
              • Message-certs-with-dest
              • Message
              • Make-certificate-messages
              • Message-set->certificate-set
              • Message-set
            • Transactions
            • Proposals
            • Validator-states
            • Blocks
            • Addresses
          • Events
          • Reachability
        • Library-extensions
      • Aleovm
      • Leo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Messages

Message-set->certificate-set

Lift message->certificate to sets.

Signature

(message-set->certificate-set msgs) → certs

Arguments

msgs — Guard (message-setp msgs).

Returns

certs — Type (certificate-setp certs).

Definitions and Theorems

Function: message-set->certificate-set

(defun message-set->certificate-set (msgs)
  (declare (xargs :guard (message-setp msgs)))
  (let ((__function__ 'message-set->certificate-set))
    (declare (ignorable __function__))
    (cond ((emptyp msgs) nil)
          (t (insert (message->certificate (head msgs))
                     (message-set->certificate-set (tail msgs)))))))

Theorem: certificate-setp-of-message-set->certificate-set

(defthm certificate-setp-of-message-set->certificate-set
  (b* ((certs (message-set->certificate-set msgs)))
    (certificate-setp certs))
  :rule-classes :rewrite)

Theorem: message->certificate-in-message-set->certificate-set

(defthm message->certificate-in-message-set->certificate-set
  (implies (in msg msgs)
           (in (message->certificate msg)
               (message-set->certificate-set msgs))))

Theorem: message-set->certificate-set-of-insert

(defthm message-set->certificate-set-of-insert
  (equal (message-set->certificate-set (insert msg msgs))
         (insert (message->certificate msg)
                 (message-set->certificate-set msgs))))

Theorem: message-set->certificate-set-of-union

(defthm message-set->certificate-set-of-union
  (equal (message-set->certificate-set (union msgs1 msgs2))
         (union (message-set->certificate-set msgs1)
                (message-set->certificate-set (sfix msgs2)))))

Theorem: message-set->certificate-set-monotone

(defthm message-set->certificate-set-monotone
  (implies (subset msgs1 msgs2)
           (subset (message-set->certificate-set msgs1)
                   (message-set->certificate-set msgs2))))

Theorem: in-of-message-set->certificate-set-of-delete

(defthm in-of-message-set->certificate-set-of-delete
  (implies (and (certificatep cert)
                (message-setp msgs)
                (in cert
                    (message-set->certificate-set msgs))
                (not (equal (message->certificate msg)
                            cert)))
           (in cert
               (message-set->certificate-set (delete msg msgs)))))