Project Website Index Table of Contents
  • Utility: Constructive Itauto Tactic
  • Utility: Classical Itauto Tactic
  • Utility: SSReflect Exports
  • Utility: General Definitions, Results and Tactics
    • Basic logic
    • Decidable propositions
    • Lemmas about transitive closure
    • Equality of dependent pairs
    • Minimal elements
    • Comparison operators
      • Reflexive comparison operators
      • Transitive comparison operators
      • Comparison operators that correspond to a strict order
      • Asymmetric comparison operators
      • Properties of compare_lt
    • Strictly ordered types
      • Comparison for subtypes
      • Comparison for options
      • Comparison for pairs and triples
      • Comparison for lists
    • Liveness
    • Misc
  • Utility: Equations Definitions
  • Utility: Finitely Supported Functions
    • Finitely supported functions on naturals
  • Utility: Natural Number Definitions and Results
    • Products of (natural) powers of integers
    • A Prime Factorization Result
  • Utility: Lemmas About Lists
    • Quantifiers for all suffixes
    • The function lastn and its properties
    • Computing longest common prefixes and suffixes
      • Longest common prefix
      • Longest common suffix
  • Utility: Std++ General Results
  • Utility: Std++ List Sets
  • Utility: List Set Definitions and Results
  • Utility: Sorted List Functions and Results
    • Sorted lists as sets
  • Utility: Finite Set Utility Definitions and Results
  • Utility: Real Number Definitions and Results
  • Utility: Topological Sorting
    • Finding an element with a minimal number of predecessors
    • Definition and properties of topologically sorted lists
    • The topological sorting algorithm
    • Maximal elements
  • Utility: Non-Empty Lists
    • Positive definition
    • List-based definition
    • Negative definition
  • Utility: Stream Definitions and Results
  • Utility: Stream Filters
    • Obtaining filtering_sequences for streams
    • Mapping a partial function on a stream
    • Mapping a function expanding elements to lists of elements on a stream
  • Utility: Definition of Possibly-Infinite Traces
    • Core trace definition and decomposition
    • Bisimulations between traces
    • Appending traces to one another
  • Utility: Properties of Possibly-Infinite Traces
    • Infiniteness property
    • Finiteness property
    • Final element properties
    • Basic trace properties and connectives
    • Basic trace element properties and connectives
    • Singleton property
    • Duplicate element property
    • Follows property
    • Append property
    • Iteration property
    • Last property
    • Midpoint property
    • Trace property operators and notations
  • Utility: Properties of Possibly-Infinite Traces Requiring Classical Logic
    • Relating finiteness and infiniteness
    • Using midpoints to show the right associativity of the append property
  • Utility: Measure Related Definitions and Results
  • Core: VLSM Basics
    • VLSM definition
      • The type of a VLSM
      • VLSM class definition
      • VLSM type definition
    • Traces
      • Valid states and messages
      • Input validity and input valid transitions
      • Valid state and valid message characterization
    • Trace Properties
      • Finite valid traces
    • Finite valid traces with a final state
      • Infinite protocol traces
      • Valid traces
      • Properties of provably-equal VLSMs
    • Alternate definitions of valid traces and states
  • Core: Preloaded VLSMs
    • Constrained traces, states and messages
    • Basic properties of preloaded VLSMs
    • Direct definitions of constrained traces, states and messages
      • Definitions of valid traces, messages, and states based on constrained ones
  • Core: VLSM Plans
  • Core: VLSM Partial Projections
    • Weak partial projection properties
    • Partial projection properties
  • Core: VLSM Stuttering Embeddings
    • Stuttering embedding definitions and properties
    • Stuttering embedding friendliness
  • Core: VLSM Total Projections
    • Projection definitions and properties
    • Projection friendliness
  • Core: VLSM Embedding
    • Weak projection properties
    • Embedding properties
    • Basic full VLSM projection
    • Weak full VLSM projection
  • Core: VLSM Inclusion
    • VLSM inclusion preservation
    • VLSM inclusion properties
  • Core: VLSM Trace Equality
    • VLSM equality properties
  • Core: VLSM Projection Properties
    • Same VLSM embedding
    • Transitivity properties
  • Core: Constrained VLSMs
  • Core: VLSM Composition
    • Free VLSM composition
    • Constrained VLSM composition
    • Lemmas about state_update
    • Lifting functions
    • A tactic for working with the state_update function
    • Basic projection lemmas
    • Binary free composition
    • Composite decidable initial message
    • Composite plan properties
    • Properties of the empty composition
    • Properties of extensionally-equal indexed compositions
    • Valid transitions in a composition
    • Valid composite states properties
  • Core: VLSM Projection Validators
    • Induced VLSM validators
    • Projection validators and Byzantine behavior
    • Transporting validator properties through VLSM embeddings/inclusions
    • Validator properties for the component_projection.
    • Direct definition of induced validator from composition to component
    • VLSM self-validation
  • Core: Composite VLSM Induced Projections
    • VLSM Projection Traces
    • Projections of Free composition of two VLSMs
    • Projection traces are Byzantine
    • A sufficient condition for the projection friendly property
    • Free composition
  • Core: Reachable Threshold
  • Core: VLSM Equivocation Definitions
    • Basic equivocation
      • State-message oracles and endowing states with history
      • Stepwise consistency properties for state_message_oracle
    • Stepwise view of HasBeenSentCapability
    • A state message oracle for messages sent or received
    • Properties of Computable Message Oracles
      • Computable (Directly) Observed Messages
      • Equivocation in compositions
  • Core: VLSM Projections and Messages Properties
    • VLSM projections reflect message properties
    • VLSM_weak_embeddings preserve message properties
    • VLSM_embeddings both preserve and reflect message properties
    • VLSM_inclusions both preserve and reflect message properties
  • Core: VLSM No-Equivocation Composition Constraints
    • No-Equivocation Invariants
    • Composite No-Equivocation Invariants
    • Preloading a VLSM composition with no equivocations constraint
  • Core: VLSM Subcomposition
    • Lifting a trace from a sub-composition to the full composition
      • Sender and sender-safety specialized for the subcomposition
    • No-equivocation results for sub-composition
    • A subcomposition with all the components
    • Relating a sub-composition with one of its components
      • A component can be lifted to a free subcomposition
      • A subcomposition can be projected to one component
    • A subcomposition with no components
  • Core: VLSM Message Dependencies
    • Equivocation Based on Message Dependencies
    • Global Equivocation Based on Message Dependencies
    • Basic validation condition for free composition
  • Core: State-Annotated VLSMs
    • Specializing projection validator properties to annotated compositions
  • Core: VLSM Byzantine Traces
    • Definition and basic properties
    • An alternative definition
    • Equivalence between the two Byzantine trace definitions
    • Byzantine fault tolerance for a single validator
    • Byzantine fault tolerance for a composition of validators
  • Core: Traceable VLSMs
    • Traceable VLSM properties
    • Composition of traceable VLSMs
  • Core: History VLSMs
  • Sufficient conditions for being a validator for the free composition
    • Message validators are validators for the free composition
    • Sufficient conditions for being a message validator for the free composition
  • Core: Fixed Set Equivocation
    • A (seemingly) stronger definition for fixed-set equivocation
    • Extending the set of components allowed to equivocate
    • Restricting Fixed valid traces to only the equivocators
    • Changing the behavior of equivocators within a trace
      • Main result of the section
    • Fixed equivocation over an empty set
  • Core: VLSM Trace-Wise Equivocation
  • Core: Witnessed Equivocation
    • Strongly witnessed equivocation
    • Witnessed equivocation and fixed-set equivocation
      • Main result of the section
  • Core: The Full Node Constraint
  • Core: VLSM Limited Message Equivocation
    • Fixed Message Equivocation implies Limited Message Equivocation
    • Limited Equivocation derived from Fixed Equivocation
  • Core: Minimally Equivocating Traces
    • The minimal equivocation choice function
    • Extracting a minimally-equivocating trace
  • Core: VLSM Equivocation
  • Core: VLSM Projecting Equivocator Traces
  • Core: VLSM Message Properties
    • Lifting properties about sent messages to the equivocators
    • Lifting the HasBeenReceivedCapability
    • Lifting the HasBeenSentCapability
    • Lifting the ComputableSentMessages property
  • Core: Equivocator State Append Determines a Projection
  • Core: VLSM Equivocator Composition
    • Extracting equivocator traces from equivocator composition traces
  • Core: VLSM Equivocator Composition Projections
  • Core: VLSM Equivocator Full Replay Traces
  • Core: Equivocators Simulating Regular Components
    • Generic simulation
    • VLSM Equivocators Simulating Free Composite
  • Core: VLSM Equivocators Fixed Equivocation
    • From composition of equivocators to composition of simple components
    • Fixed Equivocation for all Equivocators
  • Core: VLSM Equivocators Simulating Fixed Set Equivocation Composition
    • The main result
    • No-equivocation simulation as a particular case of fixed set simulation
  • Core: VLSM Limited Equivocation
  • Core: VLSM Equivocators Simulating Limited Message Equivocation Traces
  • Core: VLSM Compositions with a Fixed Set of Byzantine Components
    • A machine which can emit any valid message for a given component
      • First definition of the fixed byzantine trace property
    • Byzantine traces characterization as projections
    • Fixed Byzantine traces as traces preloaded with signed messages
      • Second fixed byzantine trace definition
    • Relation between Byzantine components and equivocators
    • The main result
  • Core: VLSM Compositions with Byzantine Components of Limited Weight
    • Assuming the byzantine components are known
    • The main result
  • Tutorial: VLSMs that Multiply
    • Definition of common features of the multiplying VLSMs
    • Definition of the doubling VLSM
      • Doubling VLSM examples
      • Doubling VLSM properties
      • Constrained messages are positive even integers
      • Constrained states property
      • Powers of 2 greater than or equal to 2 are valid messages
    • Definition of the tripling VLSM
    • Composition of doubling and tripling VLSMs
  • Tutorial: Primes Composition of VLSMs
    • Definition of the Radix VLSM
    • Radix VLSM properties
      • Constrained messages are positives divisible by the multiplier
      • Constrained states property
      • Positive powers of the multiplier are valid messages
    • A VLSM composition for all primes
      • A (slightly) constrained composition of primes
  • Tutorial: VLSMs that Generate Logical Formulas
    • Encoding formulas as VLSMs
      • VLSM for top and bottom rules
      • VLSM for the variable rule
      • VLSM for the negation rule
      • VLSM for binary connective rules
      • VLSM for expressions
    • Characterization of valid messages as formulas
    • Interpretation of formulas
  • Tutorial: Round-Based Asynchronous Muddy Children Puzzle
    • Basic definitions
    • Invariant preservation
    • Auxiliary progress results
    • Progress
    • Safety
  • ELMO: Basic Definitions and Results for UMO, MO and ELMO
    • Labels, States, Observations and Messages
    • Extending States with new Observations
      • Messages sent and received by a State
    • Observations and message dependencies
  • ELMO: Protocol Definitions and Properties for UMO
    • Component definition
    • Every valid state contains a unique valid trace leading to it
    • The suffix ordering on states is a strict total order
    • Observability
    • Protocol
  • ELMO: Protocol Definitions and Properties for MO
    • Alternative definition of validity
    • Component lemmas
      • Properties of transitions and traces
      • Extracting a trace from a state
      • State and message suffix relations
    • Protocol
      • Validators
      • Equivocation
  • ELMO: Protocol Definitions and Properties for ELMO
    • Component lemmas
    • Protocol
      • Equivocators
      • Validators
  • ELMO: Exporting of All ELMO Modules
  • Paxos: Abstract Specification of Consensus
  • Paxos: Specification of Consensus by Voting
  • Paxos: A Basic Paxos Protocol
Generated by coqdoc and improved with CoqdocJS as adapted for coq-community