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 jhendrix@galois.com.

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