Skip to content

This project contains various supporting libraries for lean to reason about protocols.

License

Notifications You must be signed in to change notification settings

GaloisInc/lean-protocol-support

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

lean-protocol-support

This repo contains various modules for lean.

The primary purpose is to help reason about network protocols, including communication between systems, serializing and deserializing messages, and some core cryptographic concepts.

Once Lean's standard library has matured, and our own contributions are more mature, we may migrate code out of this into dedicated libraries.

Galois is unable to provide support for this library. For questions, contact Joe Hendrix [email protected].

A brief summary of each module (that isn't obvious from its name) follows

  • arith: An implementation of the Fourier-Motzkin quantifier elimination procedure as a reflective tactic for deciding satisfiability of conjunctions of inequalities over Q, Z, and N
  • crypto: executable Implementations of HMAC and SHA2
    • merkle: Merkle trees, get paths through a merkle tree where the leafs are defined by a list
  • csp: A definition of communicating sequential processes
  • data: A few data libraries
    • binary: A binary tree with internal nodes
    • bounded_list: A list parameterized by a nat and a proof that length is less than that nat
    • lp_tree: A convenient datastructure for converting lists into left perfect trees whose internal nodes are defined as combinations of the leafs
    • tree: n-ary trees
  • network: Specification and implementation of a network model
    • network_monad: A monad for reading and writing to sockets
    • network_implementation: An instance of network monad
    • action, labels: A syntax for representing the actions that can occur in a network
    • agent_facts, network_local_abs: Lemmas you can apply to an agent on an abitrary network
  • sequent: Definition of intuitionistic sequents, instantiation with LTL, and tactics for derivations on intuitionistic sequents, including some reification/reflective tactics
  • subset: Defines subsets over types, and fixpoints over those subsets
  • temporal: Linear temporal logic and proof rules for interactive proving using temporal logic

About

This project contains various supporting libraries for lean to reason about protocols.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages