Cheerios: Coq Library for Serializing Data Types
Cheerios is a Coq library designed for serializing various data types with easy-to-write serializers. It offers a range of features like type classes for automatic serializer selection and combinator functions for creating serializers over different types. The project focuses on decreasing Trusted Computing Base (TCB) in Verdi and aims to improve serializer support and documentation in the future.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Cheerios Formally Verified Cerealizer Keith Simmons
What is it? A coq library for serializing data types Easy to write serializers Provides serializers of many of the coq standard library types Easy to use proof interface
Example Usage Serialization and deserialization is done through the use of type classes which allows automatic location of the correct serializer to use. In practice you either call serialize or deserialize and if the need instances exist then everything just works . Demo
Example Serializer Often when writing serializers with Cheerios one would use existing serializers to substitute for actually serializing the data. Demo
Combinators Make it easy to make serializers over other types. Mostly comes from the fact that Coq s type system is very flexible Demo
Verdi Integration Project was motivated by the need to decrease the TCB in verdi Shims are a big source of bugs and people tend to get serialization wrong Working on a Serialized VST
Future Work Finish VST for verdi Allow for serializers to return in progress as well as success and failure Better support serializers which require fuel parameters Improve documentation and website Improve extraction to use native ml binary types
