Skip to content
master
Go to file
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
doc
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

README.md

Cheerios

Build Status

Cheerios is a formally verified serialization library for Coq. It defines a typeclass for serializable types and defines instances for many built-in types. The specification of a serializable type requires that serializing followed by deserializing is the identity.

By linking extracted code with the Cheerios OCaml runtime support library, verified serializable types can be used in executable programs.

Requirements

Definitions and proofs:

Runtime:

Building

The easiest way to build and install Cheerios is via OPAM:

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam install coq-cheerios

To build Cheerios manually, first run ./configure in the root directory, and then run make.

Runtime Library

To use serializable types in executable programs, code must be extracted to OCaml and linked with the Cheerios runtime library. The connection between the Coq definitions and the runtime library primitives is established in ExtractOCamlCheeriosBasic.v in the extraction directory, which must be imported before extraction of serializable types.

Note that if a Coq type is extracted to a custom OCaml type (e.g., string to char list), extraction for serialization functions must be adjusted accordingly. Several files with such extraction directives for serialization can be found in the extraction directory.

To install the runtime library via OPAM, use the following commands:

opam repo add distributedcomponents-dev http://opam-dev.distributedcomponents.net
opam install cheerios-runtime

To compile the runtime library manually, go to the runtime directory and run make.

Projects using Cheerios

About

Formally verified Coq serialization library with support for extraction to OCaml

Topics

Resources

Releases

No releases published

Packages

No packages published
You can’t perform that action at this time.