digamma-ai/asn1fpcoq

Coq formalization of ASN.1 floating point

asn1fpcoq

ASN.1 Floating Point encoding formalized in Coq

Features

• High-level ASN.1 Real definition
• Conversion between ASN.1 and Flocq IEEE-754
• TODO: Bit-string encoding of ASN.1 real numbers

Assumptions

See doc/assumptions.md

Prerequisites

• Coq 8.8.2
• Flocq
• ExtLib
• dune
• num
• coq-bbv
• coq-compcert 3.4

To install all pre-requisites:

opam repo add coq-released http://coq.inria.fr/opam/released
opam install coq coq-ext-lib coq-flocq coq-bbv dune num core coq-compcert

Acknowledgements

• Thanks to Sylvie Boldo and Guillaume Melquiond for their development of the Floats for Coq library, on which this project heavily relies both abstractly and with code.
• Thanks to Yury Strozhevsky for the great articles explaining the basics of ASN.1 encoding.
• Thanks to all the authors and contributors of the StructTact library.