• 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
              • 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-author-next

    New correct author state resulting from a create event.

    Signature
    (create-author-next cert vstate) → new-vstate
    Arguments
    cert — Guard (certificatep cert).
    vstate — Guard (validator-statep vstate).
    Returns
    new-vstate — Type (validator-statep new-vstate).

    The input cert of this function is the certificate in the create event; see event. The input vstate is the state of the validator whose address is the certificate's author. See the (indirect) callers of this function.

    The certificate is added to the DAG.

    Definitions and Theorems

    Function: create-author-next

    (defun create-author-next (cert vstate)
      (declare (xargs :guard (and (certificatep cert)
                                  (validator-statep vstate))))
      (let ((__function__ 'create-author-next))
        (declare (ignorable __function__))
        (b* ((dag (validator-state->dag vstate))
             (new-dag (insert (certificate-fix cert) dag)))
          (change-validator-state vstate
                                  :dag new-dag))))

    Theorem: validator-statep-of-create-author-next

    (defthm validator-statep-of-create-author-next
      (b* ((new-vstate (create-author-next cert vstate)))
        (validator-statep new-vstate))
      :rule-classes :rewrite)

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

    (defthm validator-state->round-of-create-author-next
      (b* ((?new-vstate (create-author-next cert vstate)))
        (equal (validator-state->round new-vstate)
               (validator-state->round vstate))))

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

    (defthm validator-state->dag-of-create-author-next
      (b* ((?new-vstate (create-author-next cert vstate)))
        (equal (validator-state->dag new-vstate)
               (insert (certificate-fix cert)
                       (validator-state->dag vstate)))))

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

    (defthm validator-state->endorsed-of-create-author-next
      (b* ((?new-vstate (create-author-next cert vstate)))
        (equal (validator-state->endorsed new-vstate)
               (validator-state->endorsed vstate))))

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

    (defthm validator-state->last-of-create-author-next
      (b* ((?new-vstate (create-author-next cert vstate)))
        (equal (validator-state->last new-vstate)
               (validator-state->last vstate))))

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

    (defthm validator-state->blockchain-of-create-author-next
      (b* ((?new-vstate (create-author-next cert vstate)))
        (equal (validator-state->blockchain new-vstate)
               (validator-state->blockchain vstate))))

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

    (defthm validator-state->committed-of-create-author-next
      (b* ((?new-vstate (create-author-next cert vstate)))
        (equal (validator-state->committed new-vstate)
               (validator-state->committed vstate))))

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

    (defthm create-author-next-of-certificate-fix-cert
      (equal (create-author-next (certificate-fix cert)
                                 vstate)
             (create-author-next cert vstate)))

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

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

    Theorem: create-author-next-of-validator-state-fix-vstate

    (defthm create-author-next-of-validator-state-fix-vstate
      (equal (create-author-next cert (validator-state-fix vstate))
             (create-author-next cert vstate)))

    Theorem: create-author-next-validator-state-equiv-congruence-on-vstate

    (defthm
          create-author-next-validator-state-equiv-congruence-on-vstate
      (implies (validator-state-equiv vstate vstate-equiv)
               (equal (create-author-next cert vstate)
                      (create-author-next cert vstate-equiv)))
      :rule-classes :congruence)