• 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
      • Riscv
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • 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
          • Definition
            • Initialization
            • Transitions
              • Transitions-accept
              • Transitions-create
                • Create-signer-possiblep
                • Create-next
                • Create-endorsers-next
                  • Create-endorsers-possiblep
                  • Create-author-possiblep
                  • Create-possiblep
                  • Create-endorser-possiblep
                  • Create-endorser-next
                  • Create-author-next
                • Dags
                • Events-possiblep
                • Elections
                • Events-next
                • Event-next
                • Transitions-commit
                • Event-possiblep
                • Transitions-advance
                • Blockchains
                • Anchors
              • States
              • 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
    • Transitions-create

    Create-endorsers-next

    Update, in a system state, to a certificate's endorsers' states resulting from a create event.

    Signature
    (create-endorsers-next cert systate) → new-systate
    Arguments
    cert — Guard (certificatep cert).
    systate — Guard (system-statep systate).
    Returns
    new-systate — Type (system-statep new-systate).

    The input cert of this function is the certificate in the create event; see event.

    We update the states of the correct endorsers. The faulty endorsers have no internal state.

    Definitions and Theorems

    Function: create-endorsers-next-loop

    (defun create-endorsers-next-loop (cert endorsers systate)
      (declare (xargs :guard (and (certificatep cert)
                                  (address-setp endorsers)
                                  (system-statep systate))))
      (let ((__function__ 'create-endorsers-next-loop))
        (declare (ignorable __function__))
        (b* (((when (emptyp endorsers))
              (system-state-fix systate))
             (endorser (head endorsers))
             ((unless (in endorser (correct-addresses systate)))
              (create-endorsers-next-loop cert (tail endorsers)
                                          systate))
             (vstate (get-validator-state endorser systate))
             (new-vstate (create-endorser-next cert vstate))
             (new-systate
                  (update-validator-state endorser new-vstate systate)))
          (create-endorsers-next-loop cert (tail endorsers)
                                      new-systate))))

    Theorem: system-statep-of-create-endorsers-next-loop

    (defthm system-statep-of-create-endorsers-next-loop
      (b* ((new-systate
                (create-endorsers-next-loop cert endorsers systate)))
        (system-statep new-systate))
      :rule-classes :rewrite)

    Theorem: create-endorsers-next-loop-of-system-state-fix-systate

    (defthm create-endorsers-next-loop-of-system-state-fix-systate
     (equal
       (create-endorsers-next-loop cert
                                   endorsers (system-state-fix systate))
       (create-endorsers-next-loop cert endorsers systate)))

    Theorem: create-endorsers-next-loop-system-state-equiv-congruence-on-systate

    (defthm
     create-endorsers-next-loop-system-state-equiv-congruence-on-systate
     (implies
      (system-state-equiv systate systate-equiv)
      (equal (create-endorsers-next-loop cert endorsers systate)
             (create-endorsers-next-loop cert endorsers systate-equiv)))
     :rule-classes :congruence)

    Theorem: create-endorsers-next-loop-of-certificate-fix-cert

    (defthm create-endorsers-next-loop-of-certificate-fix-cert
      (equal (create-endorsers-next-loop (certificate-fix cert)
                                         endorsers systate)
             (create-endorsers-next-loop cert endorsers systate)))

    Theorem: create-endorsers-next-loop-certificate-equiv-congruence-on-cert

    (defthm
        create-endorsers-next-loop-certificate-equiv-congruence-on-cert
     (implies
      (certificate-equiv cert cert-equiv)
      (equal (create-endorsers-next-loop cert endorsers systate)
             (create-endorsers-next-loop cert-equiv endorsers systate)))
     :rule-classes :congruence)

    Theorem: correct-addresses-of-create-endorsers-next-loop

    (defthm correct-addresses-of-create-endorsers-next-loop
      (b* ((?new-systate
                (create-endorsers-next-loop cert endorsers systate)))
        (equal (correct-addresses new-systate)
               (correct-addresses systate))))

    Theorem: validator-state->round-of-create-endorsers-next-loop

    (defthm validator-state->round-of-create-endorsers-next-loop
     (b* ((?new-systate
               (create-endorsers-next-loop cert endorsers systate)))
      (equal
          (validator-state->round (get-validator-state val new-systate))
          (validator-state->round (get-validator-state val systate)))))

    Theorem: validator-state->dag-of-create-endorsers-next-loop

    (defthm validator-state->dag-of-create-endorsers-next-loop
     (b* ((?new-systate
               (create-endorsers-next-loop cert endorsers systate)))
       (equal
            (validator-state->dag (get-validator-state val new-systate))
            (validator-state->dag (get-validator-state val systate)))))

    Theorem: validator-state->endorsed-of-create-endorsers-next-loop

    (defthm validator-state->endorsed-of-create-endorsers-next-loop
     (implies
      (in val (correct-addresses systate))
      (b* ((?new-systate
                (create-endorsers-next-loop cert endorsers systate)))
       (equal
        (validator-state->endorsed
             (get-validator-state val new-systate))
        (if
         (in val endorsers)
         (insert
          (make-address+pos :address (certificate->author cert)
                            :pos (certificate->round cert))
          (validator-state->endorsed (get-validator-state val systate)))
         (validator-state->endorsed
              (get-validator-state val systate)))))))

    Theorem: validator-state->last-of-create-endorsers-next-loop

    (defthm validator-state->last-of-create-endorsers-next-loop
     (b* ((?new-systate
               (create-endorsers-next-loop cert endorsers systate)))
      (equal
           (validator-state->last (get-validator-state val new-systate))
           (validator-state->last (get-validator-state val systate)))))

    Theorem: validator-state->blockchain-of-create-endorsers-next-loop

    (defthm validator-state->blockchain-of-create-endorsers-next-loop
      (b* ((?new-systate
                (create-endorsers-next-loop cert endorsers systate)))
        (equal (validator-state->blockchain
                    (get-validator-state val new-systate))
               (validator-state->blockchain
                    (get-validator-state val systate)))))

    Theorem: validator-state->committed-of-create-endorsers-next-loop

    (defthm validator-state->committed-of-create-endorsers-next-loop
     (b* ((?new-systate
               (create-endorsers-next-loop cert endorsers systate)))
      (equal
       (validator-state->committed
            (get-validator-state val new-systate))
       (validator-state->committed (get-validator-state val systate)))))

    Theorem: get-network-state-of-create-endorsers-next-loop

    (defthm get-network-state-of-create-endorsers-next-loop
      (b* ((?new-systate
                (create-endorsers-next-loop cert endorsers systate)))
        (equal (get-network-state new-systate)
               (get-network-state systate))))

    Function: create-endorsers-next

    (defun create-endorsers-next (cert systate)
      (declare (xargs :guard (and (certificatep cert)
                                  (system-statep systate))))
      (let ((__function__ 'create-endorsers-next))
        (declare (ignorable __function__))
        (create-endorsers-next-loop cert (certificate->endorsers cert)
                                    systate)))

    Theorem: system-statep-of-create-endorsers-next

    (defthm system-statep-of-create-endorsers-next
      (b* ((new-systate (create-endorsers-next cert systate)))
        (system-statep new-systate))
      :rule-classes :rewrite)

    Theorem: correct-addresses-of-create-endorsers-next

    (defthm correct-addresses-of-create-endorsers-next
      (b* ((?new-systate (create-endorsers-next cert systate)))
        (equal (correct-addresses new-systate)
               (correct-addresses systate))))

    Theorem: validator-state->round-of-create-endorsers-next

    (defthm validator-state->round-of-create-endorsers-next
     (b* ((?new-systate (create-endorsers-next cert systate)))
      (equal
          (validator-state->round (get-validator-state val new-systate))
          (validator-state->round (get-validator-state val systate)))))

    Theorem: validator-state->dag-of-create-endorsers-next

    (defthm validator-state->dag-of-create-endorsers-next
     (b* ((?new-systate (create-endorsers-next cert systate)))
       (equal
            (validator-state->dag (get-validator-state val new-systate))
            (validator-state->dag (get-validator-state val systate)))))

    Theorem: validator-state->endorsed-of-create-endorsers-next

    (defthm validator-state->endorsed-of-create-endorsers-next
     (implies
      (in val (correct-addresses systate))
      (b* ((?new-systate (create-endorsers-next cert systate)))
       (equal
        (validator-state->endorsed
             (get-validator-state val new-systate))
        (if
         (in val (certificate->endorsers cert))
         (insert
          (make-address+pos :address (certificate->author cert)
                            :pos (certificate->round cert))
          (validator-state->endorsed (get-validator-state val systate)))
         (validator-state->endorsed
              (get-validator-state val systate)))))))

    Theorem: validator-state->last-of-create-endorsers-next

    (defthm validator-state->last-of-create-endorsers-next
     (b* ((?new-systate (create-endorsers-next cert systate)))
      (equal
           (validator-state->last (get-validator-state val new-systate))
           (validator-state->last (get-validator-state val systate)))))

    Theorem: validator-state->blockchain-of-create-endorsers-next

    (defthm validator-state->blockchain-of-create-endorsers-next
      (b* ((?new-systate (create-endorsers-next cert systate)))
        (equal (validator-state->blockchain
                    (get-validator-state val new-systate))
               (validator-state->blockchain
                    (get-validator-state val systate)))))

    Theorem: validator-state->committed-of-create-endorsers-next

    (defthm validator-state->committed-of-create-endorsers-next
     (b* ((?new-systate (create-endorsers-next cert systate)))
      (equal
       (validator-state->committed
            (get-validator-state val new-systate))
       (validator-state->committed (get-validator-state val systate)))))

    Theorem: get-network-state-of-create-endorsers-next

    (defthm get-network-state-of-create-endorsers-next
      (b* ((?new-systate (create-endorsers-next cert systate)))
        (equal (get-network-state new-systate)
               (get-network-state systate))))

    Theorem: create-endorsers-next-of-certificate-fix-cert

    (defthm create-endorsers-next-of-certificate-fix-cert
      (equal (create-endorsers-next (certificate-fix cert)
                                    systate)
             (create-endorsers-next cert systate)))

    Theorem: create-endorsers-next-certificate-equiv-congruence-on-cert

    (defthm create-endorsers-next-certificate-equiv-congruence-on-cert
      (implies (certificate-equiv cert cert-equiv)
               (equal (create-endorsers-next cert systate)
                      (create-endorsers-next cert-equiv systate)))
      :rule-classes :congruence)

    Theorem: create-endorsers-next-of-system-state-fix-systate

    (defthm create-endorsers-next-of-system-state-fix-systate
      (equal (create-endorsers-next cert (system-state-fix systate))
             (create-endorsers-next cert systate)))

    Theorem: create-endorsers-next-system-state-equiv-congruence-on-systate

    (defthm
         create-endorsers-next-system-state-equiv-congruence-on-systate
      (implies (system-state-equiv systate systate-equiv)
               (equal (create-endorsers-next cert systate)
                      (create-endorsers-next cert systate-equiv)))
      :rule-classes :congruence)