• 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
      • Taspi
      • Bitcoin
      • Riscv
      • 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
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
        • Aleobft
          • Aleobft-static
          • Aleobft-stake2
            • Correctness
            • Definition
              • Initialization
              • Transitions
              • States
              • Events
                • Event
                  • Event-case
                  • Event-fix
                  • Event-equiv
                  • Eventp
                  • Event-create
                  • Event-commit
                  • Event-advance
                  • Event-accept
                  • Event-kind
                • Messages
                • Event-list
              • Reachability
          • Aleobft-dynamic
          • Aleobft-stake
          • Aleobft-proposals
          • Library-extensions
        • Leo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Events

Event

Fixtype of events.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:create → event-create
:accept → event-accept
:advance → event-advance
:commit → event-commit

The system changes its state (see system-state) in response to the following events:

  1. A validator creates a new certificate. Note that the certificate includes the author, i.e. it indicates the validator. This adds the certificate to the DAG of the validator, and broadcasts the certificate on the network.
  2. A validator accepts a certificate, from a message in the network, which is removed from the network and added to the DAG of the validator. Note that the message indicates the validator, as the destination.
  3. A validator advances its round.
  4. A validator commits anchors.

Subtopics

Event-case
Case macro for the different kinds of event structures.
Event-fix
Fixing function for event structures.
Event-equiv
Basic equivalence relation for event structures.
Eventp
Recognizer for event structures.
Event-create
Event-commit
Event-advance
Event-accept
Event-kind
Get the kind (tag) of a event structure.