I’m happy to announce the release of ocaml-wire 0.9.0 to opam!
ocaml-wire is a set of combinators to describe binary protocols in OCaml. “Binary” as in fixed-layout: sizes and shapes are mostly known up front, so you’re reading fields at known offsets rather than parsing a free-form grammar (like in Menhir). There are already many good binary parser frameworks in OCaml – here’s what’s different in ocaml-wire:
The central data structure is EverParse’s 3D grammar. The OCaml combinators describe a 3D structure. Following Daniel’s tagged final encoding approach, you build a codec that describes a struct and how to serialise/deserialise it from an OCaml value.
Which means every description can compile down to a .3d file and from there to C via EverParse – and the generated C compiles cleanly with -std=c99 -Wall -Werror. So you could, in theory (I haven’t pushed on this too far for now), build and link a complex stack as an standalone, external C parser whose memory safety, single-pass behaviour, and conformance to the 3D spec are proven in F*(EverParse doesn’t give you serialisers, unfortunately).
If you prefer, you can still use the OCaml parsers/verifiers, which have been made reasonably fast (i.e. no extra allocations on the hot path), and as they are streaming codecs you can just read or write a single field of the structure without parsing the whole thing. They also compile trivially to JavaScript via js_of_ocaml, if you need to parse the same format in the browser.
A small example – a packet with two nibble-wide fields, a big-endian length, and a variable-size payload whose length is read from the Length field:
open Wire
type packet = { version : int; flags : int; length : int; payload : string }
let f_version = Field.v "Version" (bits ~width:4 U8)
let f_flags = Field.v "Flags" (bits ~width:4 U8)
let f_length = Field.v "Length" uint16be
let f_payload = Field.v "Payload" (byte_array ~size:(Field.ref f_length))
let codec =
let open Codec in
v "Packet" (fun version flags length payload -> { version; flags; length; payload })
[ f_version $ (fun p -> p.version);
f_flags $ (fun p -> p.flags);
f_length $ (fun p -> p.length);
f_payload $ (fun p -> p.payload) ]
Field.ref f_length is the dependent-size bit: the payload’s length comes from the f_length field read earlier in the same struct. That same codec value is what you hand to Everparse.schema to get the 3D file out, and what backs Codec.get / Codec.set for streaming field access from OCaml. ocaml-wire also ships the infrastructure for generating FFI stubs and for differential testing to make sure the verified C and hand-written OCaml parsers agree. So far they seem to
I am not familiar with the 3D formalism. What stands out is that all integers are unsigned, which reflect a bit-level view. But how can these be interpreted as signed integers or floats? Is this left to the layers above?
Yes, this is left to the layer above. The split in ocaml-wire today:
Generated C (EverParse): only sees U8, U16(BE), U32(BE), U64(BE). Checks bounds, tags, and length relations. This is the part that gets formally verified, and keeping it unsigned keeps the F* proofs tractable.
OCaml combinator layer: exposes exactly what 3D can express: the unsigned primitives, structs, bitfields, tagged unions, and dependent-size arrays. If you need a field as signed int32 or an IEEE-754 float, the conversion lives in the record constructor and per-field projection you hand to Codec.v (Int32.float_of_bits on decode, Int32.bits_of_float on encode for instance).
So the verified parser only sees the unsigned bit patterns. The signed/float interpretation is an OCaml-side convenience that EverParse has no knowledge of, so the F* proof covers memory safety, bounds, tag validity, and length relations, but not “these four bytes are a well-formed float” in any numeric sense. If you do want a semantic constraint verified, you express it at the bit level, as a constraint on the unsigned word. Tag sets and range checks drop out naturally (Field.ref f < int 0x8000_0000, or an enum disjunction); more elaborate predicates like “not a NaN” might be expressible as bitwise constraints on the exponent and mantissa, though I haven’t tried yet…
That might be a good idea to expose those bitwise constraints as first-class combinators in the DSL!
I’m happy to announce that ocaml-wire 1.0.0 is now on opam, installable with opam install wire.
This release brings a round of robustness fixes and API cleanups to the previous version (hence the 1.0.0 tag). It also adds a lot of differential testing between the OCaml parsers/serialisers and the generated verified C parsers. Both are run on randomly generated schemas and random input bytes, and the test checks that they agree on what they accept or reject, and on the values they decode. Wherever they disagreed there was a bug, and those all seem to be fixed now.
EverParse 3D has no signed or floating-point types, only unsigned integers, so to the C validator an int8 is a UINT8 and a float64 is a UINT64. The OCaml decoder does the reinterpretation, two’s complement for the signed types and IEEE 754 for the floats, and for a plain field both sides accept every bit pattern. A constraint on the field (that the user would have added via the DSL) has to survive that projection. A signed ordering constraint has to be rewritten through the two’s-complement identity before it reaches the C validator, because a naive unsigned comparison disagrees on bytes with the sign bit set (byte 200 is the signed value -56, accepted by OCaml and rejected by the naive C bound). Float finiteness (is_finite, is_nan) compiles to a test on the exponent bits, and a float ordering constraint, which has no faithful unsigned form, is rejected up front. The differential fuzzing is what surfaced those sign-bit disagreements and all of this has been hardened between 0.9 and 1.0.
Zero-copy reads got safer too. Codec.validate now enforces every check Codec.decode does (enum membership, bounds, padding, where clauses), so validating untrusted input before a batch of zero-copy Codec.get calls no longer trusts bytes the decoder would have rejected (again, caught thanks to differential testing).
The generated .3d files also turned out to be quite readable as protocol descriptions, and a whole codec family now projects to a single .3d that doubles as a spec and compiles to a standalone verified C parser with no FFI. The TCP/IP stack is a good one to compare: the OCaml definitions and the generated 3d file.
I am happy to announce the release 1.1.0 of ocaml-wire on opam!
The release improves a few things:
the generated, formally-verified parsers can now be cross-compiled (including to ocaml-freestanding to be included in a unikernel). The installed C headers are also now much smaller and only expose safe entry point.
