Hi all, I just developped Encore which, from combinators, make an `angstrom` decoder AND an encoder. By this way, we ensure isomorphism between them. You can see the project here: https://github.com/dinosaure/encore
I will integrate soon Encore to ocaml-git to ensure, again, isomorphism between Git object decoder and Git object encoder (and ensure, we don't miss something, we don't produce some noises and we produce exactly the same output from an input - and by this way, keep the same hash). I need to improve the API and may be we need to optimize encoder but it's a good start to have a safe way to produce a decoder and an encoder automatically by a description of a format. On Sun, Mar 18, 2018 at 12:39 PM Richard Mortier < [email protected]> wrote: > Came across this, might be of interest: > > https://arxiv.org/abs/1803.04870 > https://arxiv.org/pdf/1803.04870.pdf > > Narcissus: Deriving Correct-By-Construction Decoders and Encoders from > Binary Formats > Sorawit Suriyakarn, Clément Pit--Claudel, Benjamin Delaware, Adam Chlipala > (Submitted on 13 Mar 2018) > Every injective function has an inverse, although constructing the > inverse for a particular injective function can be quite tricky. One > common instance of inverse-function pairs is the binary encoders and > decoders used to convert in-memory data into and out of a structured > binary format for network communication. Ensuring that a given decoder > is a proper inverse of the original encoder is particularly important, > as any error has the potential to introduce security vulnerabilities or > to corrupt or lose data in translation. > In this paper, we present a synthesis framework, Narcissus, that > eliminates both the tedium and the potential for error in building the > inverse of a binary encoder. The starting point of the process is a > binary format, expressed as a functional program in the nondeterminism > monad, that precisely captures all the valid binary encodings of an > arbitrary datatype instance. From this specification, Narcissus > synthesizes a decoder that is guaranteed to be the inverse of this > relation, drawing on an extensible set of decoding strategies to > construct the implementation. Each decoder is furthermore guaranteed to > detect malformed encodings by failing on inputs not included in this > relation. The derivation is carried out inside the Coq proof assistant > and produces a proof trail certifying the correctness of the synthesized > decoder. We demonstrate the utility of our framework by deriving and > evaluating the performance of decoders for all packet formats used in a > standard network stack. > > ...and from the eval: > > The decoders that our framework produces are reasonably > efficient and sufficiently full-featured to be used as a drop-in > replacements for all parsing components of a typical TCP/IP > stack. We support this claim by extracting our decoders > to OCaml and integrating the resulting code into the pureOCaml > TCP/IP stack of MirageOS. > > -- > Richard Mortier > [email protected] > > _______________________________________________ > MirageOS-devel mailing list > [email protected] > https://lists.xenproject.org/mailman/listinfo/mirageos-devel >
_______________________________________________ MirageOS-devel mailing list [email protected] https://lists.xenproject.org/mailman/listinfo/mirageos-devel
