DOCSEARCHbyAlgolia
Submit Docs

CSLib

repository·main·Indexed 20 days ago

https://github.com/leanprover/cslib

A Lean library for formalizing Computer Science theories, tools, and software verification methods. CSLib provides a unified ecosystem for certified software development, featuring modules for Algorithms, Computability (including FLP impossibility), Cryptography, Logics, and Languages. It includes the Mech verified choreographic programming framework and provides foundational abstractions for semantics, labelled transition systems, and inference systems to ensure interoperability across different computational models.

Tokens
3.7K
Snippets
4
Records
26
Agent score
68%

What's inside CSLib

  1. Overview of CSLib Foundations

    main
    The Foundations directory serves as the integration hub for CSLib and downstream developments. It provides common concepts, APIs, and foundational data objects (such as Nat and Set from Mathlib) that are used across the entire library. It is designed to act as a fulcrum for integrating different parts of the library through shared abstractions.

  2. Overview of the Languages directory in CSLib

    main

    The Languages directory contains formalizations of modelling and programming languages and their properties. This includes syntax, semantics, typing, execution facilities (compilers, interpreters), behavioural theories, and supporting metatheory. The directory covers a spectrum from foundational calculi to applied programming frameworks.

    Rather than treating languages in isolation, CSLib exposes them through reusable abstractions from the Foundations directory, such as:

    • Contexts
    • Substitution
    • Congruence
    • Reduction systems
    • Labelled transition systems

  3. What is Mech: Mechanised Choreographic Programming

    main

    Mech is a verified choreographic programming framework designed for distributed systems. It allows developers to:

    1. Codify distributed protocols: Use a choreographic language that provides a simple global view of protocols (using 'Alice and Bob' notation).
    2. Reason about programs: Leverage CSLib's foundations and tools to perform formal reasoning on choreographic programs.
    3. Compile to process calculus: Transform choreographies into provably-correct models of distributed programs within a process calculus.

  4. Overview of CSLib

    main

    CSLib is a Lean library dedicated to formalizing Computer Science theories and tools. Its primary goals are to:

    • Provide APIs and languages for formalization projects, software verification, and certified software.
    • Create a common ground for connecting various Computer Science developments to foster reuse and synergy.

  5. Overview of the FLP Impossibility Formalization

    main
    This directory provides a formalization of Völzer's constructive proof of the FLP impossibility result. The FLP result states that asynchronous distributed consensus is impossible in the presence of even a single crash fault. The formalization is structured to follow the development of Völzer's proof [Volzer2004], which builds upon the original Fischer, Lynch, and Paterson [FLP1985] result.

  6. Overview of the Crypto module in CSLib

    main
    The Crypto directory provides cryptographic definitions, primitives, protocol models, and security metatheory. It is designed to support both abstract security reasoning and concrete protocol development, explicitly linking the two. The module is intended to be used in conjunction with CSLib's Languages and Logics to build end-to-end models where cryptographic operations are embedded within larger communicating or computational systems.

  8. Understand the CSLib namespace structure

    main

    CSLib is organized into several high-level namespaces that categorize computer science concepts. When building on top of the library, you can navigate its contents based on these primary domains:

    • Cslib: The root namespace containing core definitions.
      • Foundations: General-purpose definitions (complexity theory, semantics, etc.).
        • Data: General-purpose structures and types (e.g., HasFresh for types with fresh generators).
        • Control: Control flow structures (e.g., Monad, Free monads).
        • Semantics: Operational semantics, reduction systems, and program equivalences (e.g., Lts, Bisimilarity, TraceEq).
      • Logic: Logics and sequent calculi (e.g., HoareLogic, LinearLogic, LinearTemporalLogic).
      • Languages: Modeling and programming languages (e.g., Boole, CCS, LambdaCalculus, PiCalculus).
      • Computability: Automata theory and machine models (e.g., Dfa, Nfa, TuringMachine).
    • CslibTests: The directory containing the test suite for the library.

  9. Understand the structure and scope of CSLib Algorithms

    main

    The Algorithms directory is used to host algorithms and their associated properties, such as functional correctness and complexity.

    Algorithms in CSLib are organized into language-specific subdirectories based on the language they are implemented in (e.g., Boole, Lean). This allows for the study of algorithms implemented as Lean programs as well as algorithms expressed within the various Languages formalized in CSLib.

  10. How to integrate Crypto with CSLib Languages

    main
    To build end-to-end models of security protocols, cryptographic primitives in CSLib are designed to compose with the Languages module. This allows you to integrate a computational substrate (such as choreographic programming languages or process calculi) with cryptographic operations. By leveraging the common semantics APIs that connect Languages and Logics, you can formally reason about security protocols within a larger system context.

  11. How semantics abstractions work in CSLib

    main

    CSLib uses a unified approach to semantics across various domains like concurrency theory, computational models, logics, programming languages, and security protocols. Most semantic APIs are located in the Semantics directory, while the Relation directory (located at the top level) provides related foundational tools.

    By using these common abstractions, developers can:

    • Use modal and dynamic logics modularly to reason about programs.
    • Share semantic metatheory (e.g., bisimulation, trace equivalence, confluence) across different models.
    • Develop provably-correct compilers by leveraging proofs of bisimilarity or full abstraction.
    • Discover connections between disparate domains like computability, cryptography, and logic.

  12. Understand operational semantics notation (Option C)

    main

    Option C uses triangle heads (⭢) to distinguish operational semantics arrows from Lean's implication arrow (→).

    Single Semantics:

    • Reduction: m ⭢ n
    • Multi-step reduction (possibly zero): m ⯮ n
    • Transition: p μ⭢ q (where μ is a transition label)
    • Multi-step transition (possibly zero): p [μs]⯮ q (where μs is a list of labels)
    • Saturated transitions: p μ⇒ q
    • Multi-step saturated transitions: p μs➾ q

    Alternative Semantics: Suffix the arrow with the name of the relation or LTS.

    • Example reduction: m ⭢cbv n (reduction under cbv)
    • Example transition: p μ⭢late q (transition under late LTS)