OCaml Planet

The OCaml Planet aggregates various blogs from the OCaml community. If you would like to be added, read the Planet syndication HOWTO.

1203 blog posts are available. You can read the 30 more recent ones below or view older ones.

On fixed-point theorems in synthetic computability — Andrej Bauer, Nov 06, 2019

I forgot to record the fact that already two years ago I wrote a paper on Lawvere's fixed-point theorem in synthetic computability:

Andrej Bauer: On fixed-point theorems in synthetic computability. Tbilisi Mathematical Journal, Volume 10: Issue 3, pp. 167–181.

It was a special issue in honor of Professors Peter J. Freyd and F. William Lawvere on the occasion of their 80th birthdays.

Lawvere's paper "Diagonal arguments and cartesian closed categories proves a beautifully simple fixed poi…

Runners in action — Andrej Bauer, Oct 27, 2019

It has been almost a decade since Matija Pretnar and I posted the first blog posts about programming with algebraic effects and handlers and the programming language Eff. Since then handlers have become a well-known control mechanism in programming languages.

Handlers and monads excel at simulating effects, either in terms of other effects or as pure computations. For example, the familiar state monad implements mutable state with (pure) state-passing functions, and there are many more examples. But I have always felt that handlers and monads are not very good at explaining how a program interacts with its external environment and how it gets to perform real-world effects.

Danel Ahman and I have worked for a while on attacking the question on how to better model external resources and what programming constructs are appropriate for working with them. The time is right for us to show what we have done so far. The theoretical side of things is explained in our paper Runners in action, Danel implemented a Haskell library Haskell-Coop to go with the paper, and I implemented a programming language Coop.

General-purpose programming languages, even the so-called pure ones, have to have some account of interaction with the external environment. A popular choice is to provide a foreign-function interface that connects the language with an external library, and through it with an operating system and the universe. A more nuanced approach would differentiate between a function that just happens to be written in a different language, and one that actually performs an effect. The latter kind is known as an algebraic operation in the algebraic-effects-and-handlers way of doing things.

A bad approach to modeling the external world is to pretend that it is internal to the language. One would think that this is obvious but it is not. For instance, Haskell represents the interface to the external world through the IO monad. But what is this monad really? How does it get to interact with the external world? The Haskell Wiki page which answers this question has the following disclaimer:

"Warning: The following story about IO is incorrect in that it cannot actually explain some important aspects of IO (including interaction and concurrency). However, some people find it useful to begin developing an understanding."

The Wiki goes on to say how IO is a bit like a state monad with an imaginary RealWorld state, except that of course RealWorld is not really a Haskell type, or at least not one that actually holds the state of the real world.

The situation with Eff is not much better: it treats some operations at the top-level in a special way. For example, if print percolates to the top level, it turns into a real print that actually causes an effect. So it looks like there is some sort of "top level handler" that models the real world, but that cannot be the case: a handler may discard the continuation or run it twice, but Eff hardly has the ability to discard the external world, or to make it bifurcate into two separate realities.

If IO monad is not an honest monad and a top-level handler is not really a handler, then what we have is a case of ingenious hackery in need of proper programming-language design.

How precisely does an operation call in the program cause an effect in the external world? As we have just seen, some sort of runtime environment or top level needs to relate it to the external world. From the viewpoint of the program, the external world appears as state which is not directly accessible, or even representable in the language. The effect of calling an operation $\mathtt{op}(a,\kappa)$ is to change the state of the world, and to get back a result. We can model the situation with a map $\overline{\mathtt{op}} : A \times W \to B \times W$, where $W$ is the set of all states of the world, $A$ is the set of parameters, and $B$ the set of results of the operation. The operation call $\mathtt{op}(a, \kappa)$ is "executed" in the current world $w \in W$ by computing $\overline{\mathtt{op}}(a,w) = (b, w')$ to get the next world $w'$ and a result $b$. The program then proceeds with the continuation $\kappa\,b$ in the world $w'$. Notice how the world $w$ is an external entity that is manipulated by the external map $\overline{\mathtt{op}}$ realistically in a linear fashion, i.e., the world is neither discarded nor copied, just transformed.

What I have just described is not a monad or a handler, but a comodel, also known as a runner, and the map $\overline{\mathtt{op}}$ is not an operation, but a co-operation. This was all observed a while ago by Gordon Plotkin and John Power, Tarmo Uustalu, and generalized by Rasmus Møgelberg and Sam Staton, see our paper for references. Perhaps we should replace "top-level" handlers and "special" monads with runners?

Danel and I worked out how effectful runners (a generalization of runners that supports other effects in addition to state) provide a mathematical model of resource management. They also give rise to a programming concept that models top-level external resources, as well as allows programmers to modularly define their own “virtual machines” and run code inside them. Such virtual machines can be nested and combined in interesting ways. We capture the core ideas of programming with runners in an equational calculus $\lambda_{\mathsf{coop}}$, that guarantees the linear use of resources and execution of finalization code.

An interesting practical aspect of $\lambda_{\mathsf{coop}}$, that was begotten by theory, is modeling of extra-ordinary circumstances. The external environment should have the ability to signal back to the program an extra-ordinary circumstance that prevents if from returning a result. This is normally accomplished by an exception mechanism, but since the external world is stateful, there are two ways of combining it with exceptions, namely the sum and the tensor of algebraic theories. Which one is the right one? Both! After a bit of head scratching we realized that the two options are (analogous to) what is variously called "checked" and "non-checked" exceptions, errors and signals, or synchronous and asynchronous exceptions. And so we included in $\lambda_{\mathsf{coop}}$ both mechanisms: ordinary exceptions, which are special events that disrupt the flow of user code but can be caught and attended to, and signals which are unrecoverable failures that irrevocably kill user code, but can still be finalized. We proved a finalization theorem which gives strong guarantees about resources always being properly finalized.

If you are familiar with handlers, as a first approximation you can think of runners as handlers that use the continuation at most once in a tail-call position. Many handlers are already of this form but not all. Non-determinism, probability, and handlers that hijack the continuation (delimcc, threads, and selection functionals) fall outside of the scope of runners. Perhaps in the future we can resurrect some of these (in particular it seems like threads, or even some form of concurrency would be worth investigating). There are many other directions of possible future investigations: efficient compilation, notions of correctness, extensions to the simple effect subtyping discipline that we implemented, etc.

To find out more, we kindly invite you to have a look at the paper, and to try out the implementations. The prototype programming language Coop implements and extends $\lambda_{\mathsf{coop}}$. You can start by skimming the Coop manual and the examples. If you prefer to experiment on your own, you might prefer the Haskell-Coop library, as it allows you to combine runners with everything else that Haskell has to offer.

Hide

Coq 8.10.1 is out — Coq, Oct 25, 2019

The 8.10.1 release of Coq is available.

Main changes:

fix proof of False when using SProp;
fix an anomaly when unsolved evar in Add Ring;
fix Ltac regression in binding free names in uconstr;
fix handling of unicode input before space;
fix custom extraction of inductives to JSON.

All details can be found in the user manual.

Feedback and bug reports are extremely welcome.

Announcing MirageOS 3.6.0 — MirageOS (Martin Lucina), Oct 18, 2019

MirageOS 3.6.0 release

We are pleased to announce the release of MirageOS 3.6.0. This release updates MirageOS to support Solo5 0.6.0 and later.

New features:

Support for the Solo5 spt (sandboxed process tender) target via mirage configure -t spt. The spt target runs MirageOS unikernels in a minimal strict seccomp sandbox on Linux x86_64, aarch64 and ppc64le hosts.
Support for the Solo5 application manifest, enabling support for multiple network and block storage devices on the hvt, spt and muen

Commas in big numbers everywhere: An OpenType adventure — Jane Street, Oct 14, 2019

My job involves a lot of staring at large numbers, mostly latencies in nanoseconds, and picking out magnitudes like microseconds. I noticed myself constantly counting digits in my text editor, in my terminal, and in Jupyter notebooks in my browser.

Coq 8.10.0 is out — Coq, Oct 07, 2019

The 8.10.0 release of Coq is available.

Main changes:

some quality-of-life bug fixes;
a critical bug fix related to template polymorphism;
native 63-bit machine integers;
a new sort of definitionally proof-irrelevant propositions: SProp;
private universes for opaque polymorphic constants;
string notations and numeral notations;
a new simplex-based proof engine for the tactics lia, nia, lra and nra;
new introduction patterns for SSReflect;
a tactic to rewrite under binders: under;
easy input of…

OCaml expert and beginner training by OCamlPro (in French): Nov. 5-6 & 7-8 — OCamlPro, Sep 25, 2019

In our endeavour to encourage professional programmers to understand and use OCaml, OCamlPro will be giving two training sessions, in French, in our Paris offices:

OCaml Beginner course for professional programmers (5-6 Nov)
OCaml Expertise (7-8 Nov).

The “Expert” OCaml course is for already experienced OCaml programmers to better understand advanced type system possibilities (objects, GADTs), discover GC internals, write “compiler-optimizable” code.

These sessions are …

Mr. MIME - Parse and generate emails — Tarides (Romain Calascibetta), Sep 25, 2019

We're glad to announce the first release of `mrmime`, a parser and a generator of emails. This library provides an OCaml way to analyze and craft an email. The eventual goal is to build an entire unikernel-compatible stack for email (such as SMTP or IMAP).

In this article, we will show what is currently possible with mrmime and present a few of the useful libraries that we developed along the way.

An email parser

Some years ago, Romain gave a talk about what an email really is. Behind the h…

In this article, we will show what is currently possible with mrmime and present a few of the useful libraries that we developed along the way.

An email parser

Some years ago, Romain gave a talk about what an email really is. Behind the human-comprehensible format (or rich-document as we said a long time ago), there are several details of emails which complicate the process of analyzing them (and can be prone to security lapses). These details are mostly described by three RFCs:

Even though they are cross-compatible, providing full legacy email parsing is an archaeological exercise: each RFC retains support for the older design decisions (which were not recognized as bad or ugly in 1970 when they were first standardized).

The latest email-related RFC (RFC5322) tried to fix the issue and provide a better formal specification of the email format – but of course, it comes with plenty of obsolete rules which need to be implemented. In the standard, you find both the current grammar rule and its obsolete equivalent.

An extended email parser

Even if the email format can defined by "only" 3 RFCs, you will miss email internationalization (RFC6532), the MIME format (RFC2045, RFC2046, RFC2047, RFC2049), or certain details needed to be interoperable with SMTP (RFC5321). There are still more RFCs which add extra features to the email format such as S/MIME or the Content-Disposition field.

Given this complexity, we took the most general RFCs and tried to provide an easy way to deal with them. The main difficulty is the multipart parser, which deals with email attachments (anyone who has tried to make an HTTP 1.1 parser knows about this).

A realistic email parser

Respecting the rules described by RFCs is not enough to be able to analyze any email from the real world: existing email generators can, and do, produce non-compliant email. We stress-tested mrmime by feeding it a batch of 2 billion emails taken from the wild, to see if it could parse everything (even if it does not produce the expected result). Whenever we noticed a recurring formatting mistake, we updated the details of the ABNF to enable mrmime to parse it anyway.

A parser usable by others

One demonstration of the usability of mrmime is `ocaml-dkim`, which wants to extract a specific field from your mail and then verify that the hash and signature are as expected.

ocaml-dkim is used by the latest implementation of `ocaml-dns` to request public keys in order to verify email.

The most important question about ocaml-dkim is: is it able to verify your email in one pass? Indeed, currently some implementations of DKIM need 2 passes to verify your email (one to extract the DKIM signature, the other to digest some fields and bodies). We focused on verifying in a single pass in order to provide a unikernel SMTP relay with no need to store your email between verification passes.

An email generator

OCaml is a good language for making little DSLs for specialized use-cases. In this case, we took advantage of OCaml to allow the user to easily craft an email from nothing.

The idea is to build an OCaml value describing the desired email header, and then let the Mr. MIME generator transform this into a stream of characters that can be consumed by, for example, an SMTP implementation. The description step is quite simple:

#require "mrmime" ;;
#require "ptime.clock.os" ;;

open Mrmime

let romain_calascibetta =
  let open Mailbox in
  Local.[ w "romain"; w "calascibetta" ] @ Domain.(domain, [ a "gmail"; a "com" ])

let john_doe =
  let open Mailbox in
  Local.[ w "john" ] @ Domain.(domain, [ a "doe"; a "org" ])
  |> with_name Phrase.(v [ w "John"; w "D." ])

let now () =
  let open Date in
  of_ptime ~zone:Zone.GMT (Ptime_clock.now ())

let subject =
  Unstructured.[ v "A"; sp 1; v "Simple"; sp 1; v "Mail" ]

let header =
  let open Header in
  Field.(Subject $ subject)
  & Field.(Sender $ romain_calascibetta)
  & Field.(To $ Address.[ mailbox john_doe ])
  & Field.(Date $ now ())
  & empty

let stream = Header.to_stream header

let () =
  let rec go () =
    match stream () with
    | Some buf -> print_string buf; go ()
    | None -> ()
  in
  go ()

This code produces the following header:

Date: 2 Aug 2019 14:10:10 GMT
To: John "D." <john@doe.org>
Sender: romain.calascibetta@gmail.com
Subject: A Simple Mail

78-character rule

One aspect about email and SMTP is about some historical rules of how to generate them. One of them is about the limitation of bytes per line. Indeed, a generator of mail should emit at most 80 bytes per line - and, of course, it should emits entirely the email line per line.

So mrmime has his own encoder which tries to wrap your mail into this limit. It was mostly inspired by Faraday and Format powered with GADT to easily describe how to encode/generate parts of an email.

A multipart email generator

Of course, the main point about email is to be able to generate a multipart email - just to be able to send file attachments. And, of course, a deep work was done about that to make parts, compose them into specific Content-Type fields and merge them into one email.

Eventually, you can easily make a stream from it, which respects rules (78 bytes per line, stream line per line) and use it directly into an SMTP implementation.

This is what we did with the project `facteur`. It's a little command-line tool to send with file attachement mails in pure OCaml - but it works only on an UNIX operating system for instance.

Behind the forest

Even if you are able to parse and generate an email, more work is needed to get the expected results.

Indeed, email is a exchange unit between people and the biggest deal on that is to find a common way to ensure a understable communication each others. About that, encoding is probably the most important piece and when a French person wants to communicate with a latin1 encoding, an American person can still use ASCII.

Rosetta

So about this problem, the choice was made to unify any contents to UTF-8 as the most general encoding of the world. So, we did some libraries which map an encoding flow to Unicode code-point, and we use uutf (thanks to dbuenzli) to normalize it to UTF-8.

The main goal is to avoid a headache to the user about that and even if contents of the mail is encoded with latin1 we ensure to translate it correctly (and according RFCs) to UTF-8.

This project is `rosetta` and it comes with:

`uuuu` for ISO-8859 encoding
`coin` for KOI8-{R,U} encoding
`yuscii` for UTF-7 encoding

Pecu and Base64

Then, bodies can be encoded in some ways, 2 precisely (if we took the main standard):

A base64 encoding, used to store your file
A quoted-printable encoding

So, about the base64 package, it comes with a sub-package base64.rfc2045 which respects the special case to encode a body according RFC2045 and SMTP limitation.

Then, pecu was made to encode and decode quoted-printable contents. It was tested and fuzzed of course like any others MirageOS's libraries.

These libraries are needed for an other historical reason which is: bytes used to store mail should use only 7 bits instead of 8 bits. This is the purpose of the base64 and the quoted-printable encoding which uses only 127 possibilities of a byte. Again, this limitation comes with SMTP protocol.

Conclusion

mrmime is tackling the difficult task to parse and generate emails according to 50 years of usability, several RFCs and legacy rules. So, it still is an experimental project. We reach the first version of it because we are currently able to parse many mails and then generate them correctly.

Of course, a bug (a malformed mail, a server which does not respect standards or a bad use of our API) can appear easily where we did not test everything. But we have the feeling it was the time to release it and let people to use it.

The best feedback about mrmime and the best improvement is yours. So don't be afraid to use it and start to hack your emails with it.

Hide

A look back on OCaml since 2011 — OCamlPro, Sep 20, 2019

As you already know if you’ve read our last blogpost, we have updated our OCaml cheat sheets starting with the language and stdlib ones. We know some of you have students to initiate in September and we wanted these sheets to be ready for the start of the school year! We’re working on more sheets for OCaml tools like opam or Dune and important libraries such as Obj Lwt or Core. Keep an eye on our blog or the repo on GitHub to follow all the updates.

Going through the documentation was a jour…

Going through the documentation was a journey to the past: we have looked back on 8 years of evolution of the OCaml language and library. New feature after new feature, OCaml has seen many changes. Needless to say, upgrading our cheat sheets to OCaml 4.08.1 was a trip down memory lane. We wanted to share our throwback experience with you!

2011

Fabrice Le Fessant first published our cheat sheets in 2011, the year OCamlPro was created! At the time, OCaml was in its 3.12 version and just got its current name agreed upon. First-class modules were the new big thing, Camlp4 and Camlp5 were battling for the control of the syntax extension world and Godi and Oasis were the packaging rage.

2012

Right after 3.12 came the switch to OCaml 4.00 which brought a major change: GADTs (generalized algebraic data types). Most of OCaml’s developers don’t use their almighty typing power, but the possibilities they provide are really helpful in some cases, most notably the format overhaul. They’re also a fun way to troll a beginner asking how to circumvent the typing system on Stack Overflow. Since most of us might lose track of their exact syntax, GADTs deserve their place in the updated sheet (if you happen to be OCamlPro’s CTO, of course the writer of this blogpost remembers how to use GADTs at all times).

On the standard library side, the big change was the switch of Hashtbl to Murmur 3 and the support for seeded randomization.

2013

With OCaml 4.01 came constructor disambiguation, but there isn’t really a way to add this to the sheet. This feature allows you to avoid misguided usage of polymorphic variants, but that’s a matter of personal taste (there’s a well-known rule that if you refresh the comments section enough times, someone —usually called Daniel— will appear to explain polymorphic variants’ superiority to you). -ppx rewriters were introduced in this version as well.

The standard library got a few new functions. Notably, Printexc.get_callstack for stack inspection, the optimized application operators |> and @@ and Format.asprintf.

2014

Gabriel Scherer, on the Caml-list, end of January:

TL;DR: During the six next months, we will follow pull requests (PR) posted on the github mirror of the OCaml distribution, as an alternative to the mantis bugtracker. This experiment hopes to attract more people to participate in the extremely helpful and surprisingly rewarding activity of patch reviews.

Can you guess which change to the cheat-sheets came with 4.02? It’s a universally-loved language feature added in 2014. Still don’t know? It is exceptional! Got it?

Drum roll… it is the match with exception construction! It made our codes simpler, clearer and in some cases more efficient. A message to people who want to improve the language: please aim for that.

This version also added the {quoted|foo|quoted} syntax (which broke comments), generative functors, attributes and extension nodes, extensible data types, module aliases and, of course, immutable strings (which was optional at the time). Immutable strings is the one feature that prompted us to remove a line from the cheat sheets. More space is good. Camlp4 and Labltk moved out of the distribution.

In consequence of immutable strings, Bytes and BytesLabel were added to the library. For the great pleasure of optimization addicts, raise_notrace popped up. Under the hood, the format type was re-implemented using GADTs.

2015

This release was so big that 4.02.2 feels like a release in itself, with the adding of nonrec and #... operators.

The standard library was spared by this bug-fix themed release. Note that this is the last comparatively slow year of OCaml as the transition to GitHub would soon make features multiply, as hindsight teaches us.

2016

Speaking of a major release, we’re up to OCaml 4.03! It introduced inline records, a GADT exhaustiveness check on steroids (with -> . to denote unreachability) and standard attributes like warning, inlined, unboxed or immediate. Colors appeared in the compiler and last but not least, it was the dawn of a new option called Flambda.

The library saw a lot of useful new functions coming in: lots of new iterators for Array, an equal function in most basic type modules, Uchar, the *_ascii alternatives and, of course, Ephemeron.

4.04 was much more restrained, but it was the second release in a single year. Local opening of module with the M.{} syntax was added along with the let exception ... in construct. String.split_on_char was notably added to the stdlib which means we don’t have to rewrite it anymore.

2017

We now get to 4.05… which did not change the language. Not that the development team wasn’t busy, OCaml just got better without any change to the syntax.

On the library side however, much happened, with the adding of *_opt functions pretty much everywhere. If you’re using the OCaml compiler from Debian, this is where you might think the story ends. You’d be wrong…

…because 4.06 added a lot! My own favorite feature from this release has to be user-defined indexing operators. This is also when safe-string became the default, giving worthwhile work to every late maintainer in the community. This release also added one awesome function in the standard library: Map.update.

2018

4.07 was aimed towards solidifying the language. It added empty variants and type-based selection of GADT constructors to the mix.

On the library side, one old and two new modules were added, with the integration of Bigarray, Seq and Float.

2019

And here we are with 4.08, in the present day! We can now put exceptions under or-patterns, which is the only language change from this release we propagated to the sheet. Time will tell if we need to add custom binding operators or [@@alert]. Pervasives is now deprecated in profit of Stdlib and new modules are popping up (Int, Bool, Fun, Result… did we miss one?) while Sort made its final deprecation warning.

We did not add 4.09 to this journey to the past, as this release is still solidly in the now at the time of this blogpost. Rest assured, we will see much more awesome features in OCaml in the future! In the meantime, we are working on updating more cheat sheets: keep posted!

Hide

Frama-C 19.1 (Potassium) is out. Download ithere. — Frama-C, Sep 17, 2019

Coq 8.10+beta3 is out — Coq, Sep 16, 2019

The third beta release of Coq 8.10 is available for testing.

This third β version includes various bug fixes and improvements, including:

improved warning on coercion path ambiguity;
support for OCaml extraction of primitive machine integers;
fix for the soundness issue with template polymorphism;
fix extraction of dependent record projections to OCaml.

More details are given in the user manual.

Feedback and bug reports are extremely welcome.

OCaml Developer at Ahrefs Pte Ltd (Full-time) — Functional Jobs (FunctionalJobs.com), Sep 14, 2019

What We Need

Ahrefs is looking for a backend developer with deep understanding of networks, distributed systems, OS fundamentals and taste for simple and efficient architectural designs. Our backend is mostly implemented in OCaml with some C++ and Rust.

In this role, be prepared to deal with 25 petabytes of live data, OCaml and Linux on a daily basis.

Basic Requirements:

Proficiency in OCaml
Knowledge of C++ and/or Rust is a plus

The ideal candidate is expected to:

Independently deal wi…

What We Need

In this role, be prepared to deal with 25 petabytes of live data, OCaml and Linux on a daily basis.

Basic Requirements:

Proficiency in OCaml
Knowledge of C++ and/or Rust is a plus

The ideal candidate is expected to:

Independently deal with bugs, schedule tasks and investigate code
Make well-reasoned technical choices and take responsibility for them
Understand the whole technology stack at all levels: from network and user-space code to OS internals and hardware
Handle full development cycle of a single component i.e. formalize task, write code and tests, setup and support production, resolve user requests
Approach problems with a practical mindset and suppress perfectionism when time is a priority
Write flexible, maintainable code and adapt to post-launch requirements/tweaks

These requirements stem naturally from our approach to development with fast feedback cycle, highly-focused personal areas of responsibility and strong tendency to vertical component splitting.

If your preference is leaning towards making the web functional and working on user-facing stuff, you may want to consider our ReasonML position instead.

Who We Are

Ahrefs runs an internet-scale bot that crawls the whole web 24/7, storing huge volumes of information to be indexed and structured in a timely fashion. Our backend system is powered by a custom petabyte-scale distributed key-value storage to accommodate all that data coming in at high speed. With this data, Ahrefs builds analytics services for end-users in the Search Engine Optimization (SEO) space and a web-scale search platform.

We are a lean and robust team who strongly believe that better technology leads to better solutions for real-world problems. We worship functional languages and static typing, extensively employ code generation and meta-programming, value code clarity and predictability, and are constantly seeking to automate repetitive tasks and eliminate boilerplate, guided by DRY and following KISS. If there is any new technology that will make our life easier - no doubt, we'll give it a try. We rely heavily on opensource code (as the only viable way to build maintainable system) and contribute back, see e.g. https://github.com/ahrefs . It goes without saying that our team is all passionate and experienced OCaml programmers, ready to lend a hand and explain that intricate ocamlbuild rule or track down a CPU bug.

Our motto is "first do it, then do it right, then do it better".

What You Get

We offer: - Competitive compensation package - Informal and thriving work atmosphere - [SG office] First-class workplace equipment (hardware & tools) - Above-average perks and fringe benefits

Work location for this role could be: - Singapore - Remote

Get information on how to apply for this position.

Hide

Compiler Engineer at Axoni (Full-time) — Functional Jobs (FunctionalJobs.com), Sep 13, 2019

Compiler Engineer

Headquartered in New York City, we are currently working intensely on what we expect to become the most widely used programming language for blockchain smart contracts: AxLang. Based on Scala, AxLang enables secure and full featured smart contract development by supporting both functional programming and formal verification. Its design is driven by the rigorous requirements for solutions serving the world's largest financial institutions.

AxLang is part of Axoni's b…

Updated Cheat Sheets: OCaml Language and OCaml Standard Library — OCamlPro, Sep 13, 2019

In 2011, we shared several cheat sheets for OCaml. Cheat sheets are helpful to refer to, as an overview of the documentation when you are programming, especially when you’re starting in a new language. They are meant to be printed and pinned on your wall, or to be kept in handy on a spare screen. We hope they will help you out when your rubber duck is rubbish at debugging your code!

Since we first shared them, OCaml and its related tools have evolved. We decided to refresh them and started…

Frama-Clang 0.0.7 is out. Download ithere. — Frama-C, Sep 13, 2019

Decompress: Experiences with OCaml optimization — Tarides (Romain Calascibetta), Sep 13, 2019

In our first article we mostly discussed the API design of decompress and did not talk too much about the issue of optimizing performance. In this second article, we will relate our experiences of optimizing decompress.

As you might suspect, decompress needs to be optimized a lot. It was used by several projects as an underlying layer of some formats (like Git), so it can be a real bottleneck in those projects. Of course, we start with a footgun by using a garbage-collected language; comparing t…

However, using something like decompress instead of C implementations can be very interesting for many purposes, especially when thinking about unikernels. As we said in the previous article, we can take the advantage of the runtime and the type-system to provide something safer (of course, it's not really true since zlib has received several security audits).

The main idea in this article is not to give snippets to copy/paste into your codebase but to explain some behaviors of the compiler / runtime and hopefully give you some ideas about how to optimize your own code. We'll discuss the following optimizations:

specialization
inlining
untagged integers
exceptions
unrolling
hot-loop
caml_modify
representation sizes

Cautionary advice

Before we begin discussing optimization, keep this rule in mind:

Only perform optimization at the end of the development process.

An optimization pass can change your code significantly, so you need to keep a state of your project that can be trusted. This state will provide a comparison point for both benchmarks and behaviors. In other words, your stable implementation will be the oracle for your benchmarks. If you start with nothing, you'll achieve arbitrarily-good performance at the cost of arbitrary behavior!

We optimized decompress because we are using it in bigger projects for a long time (2 years). So we have an oracle (even if zlib can act as an oracle in this special case).

Specialization

One of the biggest specializations in decompress is regarding the min function. If you don't know, in OCaml min is polymorphic; you can compare anything. So you probably have some concerns about how min is implemented?

You are right to be concerned: if you examine the details, min calls the C function do_compare_val, which traverses your structure and does a comparison according the run-time representation of your structure. Of course, for integers, it should be only a cmpq assembly instruction. However, some simple code like:

let x = min 0 1

will produce this CMM and assembly code:

(let x/1002 (app{main.ml:1,8-15} "camlStdlib__min_1028" 1 3 val)
   ...)

.L101:
        movq    $3, %rbx
        movq    $1, %rax
        call    camlStdlib__min_1028@PLT

Note that beta-reduction, inlining and specialization were not done in this code. OCaml does not optimize your code very much – the good point is predictability of the produced assembly output.

If you help the compiler a little bit with:

external ( <= ) : int -> int -> bool = "%lessequal"
let min a b = if a <= b then a else b [@@inline]

let x = min 0 1

We have:

(function{main.ml:2,8-43} camlMain__min_1003 (a/1004: val b/1005: val)
 (if (<= a/1004 b/1005) a/1004 b/1005))

(function camlMain__entry ()
 (let x/1006 1 (store val(root-init) (+a "camlMain" 8) 1)) 1a)

.L101:
        cmpq    %rbx, %rax
        jg      .L100
        ret

So we have all optimizations, in this produced code, x was evaluated as 0 (let x/... (store ... 1)) (beta-reduction and inlining) and min was specialized to accept only integers – so we are able to emit cmpq.

Results

With specialization, we won 10 Mb/s on decompression, where min is used in several places. We completely avoid an indirection and a call to the slow do_compare_val function.

This kind of specialization is already done by `flambda`, however, we currently use OCaml 4.07.1. So we decided to this kind of optimization by ourselves.

Inlining

In the first example, we showed code with the [@@inline] keyword which is useful to force the compiler to inline a little function. We will go outside the OCaml world and study C code (gcc 5.4.0) to really understand inlining.

In fact, inlining is not necessarily the best optimization. Consider the following (nonsensical) C program:

#include <stdio.h>
#include <string.h>
#include <unistd.h>
#include <time.h>
#include <stdlib.h>

#ifdef HIDE_ALIGNEMENT
__attribute__((noinline, noclone))
#endif
void *
hide(void * p) { return p; }

int main(int ac, const char *av[])
{
  char *s = calloc(1 << 20, 1);
  s = hide(s);

  memset(s, 'B', 100000);

  clock_t start = clock();

  for (int i = 0; i < 1280000; ++i)
    s[strlen(s)] = 'A';

  clock_t end = clock();

  printf("%lld\n", (long long) (end-start));

  return 0;
}

We will compile this code with -O2 (the second level of optimization in C), once with -DHIDE_ALIGNEMENT and once without. The assembly emitted differs:

.L3:
    movq    %rbp, %rdi
    call    strlen
    subl    $1, %ebx
    movb    $65, 0(%rbp,%rax)
    jne    .L3

.L3:
    movl    (%rdx), %ecx
    addq    $4, %rdx
    leal    -16843009(%rcx), %eax
    notl    %ecx
    andl    %ecx, %eax
    andl    $-2139062144, %eax
    je    .L3

In the first output (with -DHIDE_ALIGNEMENT), the optimization pass decides to disable inlining of strlen; in the second output (without -DHIDEAlIGNEMENT), it decides to inline strlen (and do some other clever optimizations). The reason behind this complex behavior from the compiler is clearly described here.

But what we want to say is that inlining is not an automatic optimization; it might act as a pessimization. This is the goal of flambda: do the right optimization under the right context. If you are really curious about what gcc does and why, even if it's very interesting, the reverse engineering of the optimization process and which information is relevant about the choice to optimize or not is deep, long and surely too complicated.

A non-spontaneous optimization is to annotate some parts of your code with [@@inline never] – so, explicitly say to the compiler to not inline the function. This constraint is to help the compiler to generate a smaller code which will have more chance to fit under the processor cache.

For all of these reasons, [@@inline] should be used sparingly and an oracle to compare performances if you inline or not this or this function is necessary to avoid a pessimization.

In `decompress`

Inlining in decompress was done on small functions which need to allocate to return a value. If we inline them, we can take the opportunity to store returned value in registers (of course, it depends how many registers are free).

As we said, the goal of the inflator is to translate a bit sequence to a byte. The largest bit sequence possible according to RFC 1951 has length 15. So, when we process an inputs flow, we eat it 15 bits per 15 bits. For each packet, we want to recognize an existing associated bit sequence and then, binded values will be the real length of the bit sequence and the byte:

val find : bits:int -> { len: int; byte: int; }

So for each call to this function, we need to allocate a record/tuple. It's why we choose to inline this function. min was inlined too and some other small functions. But as we said, the situation is complex; where we think that inlining can help us, it's not systematically true.

NOTE: we can recognize bits sequence with, at most, 15 bits because a Huffman coding is prefix-free.

Untagged integers

When reading assembly, the integer 0 is written as $1. It's because of the GC bit needed to differentiate a pointer and an unboxed integer. This is why, in OCaml, we talk about a 31-bits integer or a 63-bits integer (depending on your architecture).

We will not try to start a debate about this arbitrary choice on the representation of an integer in OCaml. However, we can talk about some operations which can have an impact on performances.

The biggest example is about the mod operation. Between OCaml and C, % or mod should be the same:

let f a b = a mod b

The output assembly is:

.L105:
        movq    %rdi, %rcx
        sarq    $1, %rcx     // b >> 1
        movq    (%rsp), %rax
        sarq    $1, %rax     // a >> 1
        testq   %rcx, %rcx   // b != 0
        je      .L107
        cqto
        idivq   %rcx         // a % b
        jmp     .L106
.L107:
        movq    caml_backtrace_pos@GOTPCREL(%rip), %rax
        xorq    %rbx, %rbx
        movl    %ebx, (%rax)
        movq    caml_exn_Division_by_zero@GOTPCREL(%rip), %rax
        call    caml_raise_exn@PLT
.L106:
        salq    $1, %rdx     // x << 1
        incq    %rdx         // x + 1
        movq    %rbx, %rax

where idiomatically the same C code produce:

.L2:
        movl    -12(%rbp), %eax
        cltd
        idivl   -8(%rbp)
        movl    %edx, -4(%rbp)

Of course, we can notice firstly the exception in OCaml (Divided_by_zero) - which is pretty good because it protects us against an interrupt from assembly (and keep the trace). Then, we need to untag a and b with sarq assembly operation. We do, as the C code, idiv and then we must retag returned value x with salq and incq.

So in some parts, it should be more interesting to use Nativeint. However, by default, a nativeint is boxed. boxed means that the value is allocated in the OCaml heap alongside a header.

Of course, this is not what we want so, if our nativeint ref (to have side-effect, like x) stay inside a function and then, you return the real value with the deref ! operator, OCaml, by a good planet alignment, can directly use registers and real integers. So it should be possible to avoid these needed conversions.

Readability versus performance

We use this optimization only in few parts of the code. In fact, switch between int and nativeint is little bit noisy:

hold := Nativeint.logor !hold Nativeint.(shift_left (of_int (unsafe_get_uint8 d.i !i_pos)) !bits)

In the end, we only gained 0.5Mb/s of inflation rate, so it's not worthwhile to do systematically this optimization. Especially that the gain is not very big. But this case show a more troubling problem: loss of readability.

In fact, we can optimize more and more a code (OCaml or C) but we lost, step by step, readability. You should be afraid by the implementation of strlen for example. In the end, the loss of readability makes it harder to understand the purpose of the code, leading to errors whenever some other person (or you in 10 years time) tries to make a change.

And we think that this kind of optimization is not the way of OCaml in general where we prefer to produce an understandable and abstracted code than a cryptic and super fast one.

Again, flambda wants to fix this problem and let the compiler to do this optimization. The goal is to be able to write a fast code without any pain.

Exceptions

If you remember our article about the release of base64, we talked a bit about exceptions and used them as a jump. In fact, it's pretty common for an OCaml developer to break the control-flow with an exception. Behind this common design/optimization, it's about calling convention.

Indeed, choose the jump word to describe OCaml exception is not the best where we don't use setjmp/longjmp.

In the details, when you start a code with a try .. with, OCaml saves a trap in the stack which contains information about the with, the catcher. Then, when you raise, you jump directly to this trap and can just discard several stack frames (and, by this way, you did not check each return codes).

In several places and mostly in the hot-loop, we use this pattern. However, it completely breaks the control flow and can be error-prone.

To limit errors and because this pattern is usual, we prefer to use a local exception which will be used only inside the function. By this way, we enforce the fact that exception should not (and can not) be caught by something else than inside the function.

    let exception Break in

    ( try while !max >= 1 do
          if bl_count.(!max) != 0 then raise_notrace Break
        ; decr max done with Break -> () ) ;

This code above produce this assembly code:

.L105:
        pushq   %r14
        movq    %rsp, %r14
.L103:
        cmpq    $3, %rdi              // while !max >= 1
        jl      .L102
        movq    -4(%rbx,%rdi,4), %rsi // bl_count,(!max)
        cmpq    $1, %rsi              // bl_count.(!max) != 0
        je      .L104
        movq    %r14, %rsp
        popq    %r14
        ret                           // raise_notrace Break
.L104:
        addq    $-2, %rdi             // decr max
        movq    %rdi, 16(%rsp)
        jmp     .L103

Where the ret is the raise_notrace Break. A raise_notrace is needed, otherwise, you will see:

        movq    caml_backtrace_pos@GOTPCREL(%rip), %rbx
        xorq    %rdi, %rdi
        movl    %edi, (%rbx)
        call    caml_raise_exn@PLT

Instead the ret assembly code. Indeed, in this case, we need to store where we raised the exception.

Unrolling

When we showed the optimization done by gcc when the string is aligned, gcc did another optimization. Instead of setting the string byte per byte, it decides to update it 4 bytes per 4 bytes.

This kind of this optimization is an unroll and we did it in decompress. Indeed, when we reach the copy opcode emitted by the lz77 compressor, we want to blit length byte(s) from a source to the outputs flow. It can appear that this memcpy can be optimized to copy 4 bytes per 4 bytes – 4 bytes is generally a good idea where it's the size of an int32 and should fit under any architectures.

let blit src src_off dst dst_off =
  if dst_off – src_off < 4
  then slow_blit src src_off dst dst_off
  else
    let len0 = len land 3 in
    let len1 = len asr 2 in

    for i = 0 to len1 – 1
    do
      let i = i * 4 in
      let v = unsafe_get_uint32 src (src_off + i) in
      unsafe_set_uint32 dst (dst_off + i) v ;
    done ;

    for i = 0 to len0 – 1
    do
      let i = len1 * 4 + i in
      let v = unsafe_get_uint8 src (src_off + i) in
      unsafe_set_uint8 dst (dst_off + i) v ;
    done

In this code, at the beginning, we copy 4 bytes per 4 bytes and if len is not a multiple of 4, we start the trailing loop to copy byte per byte then. In this context, OCaml can unbox int32 and use registers. So this function does not deal with the heap, and by this way, with the garbage collector.

Results

In the end, we gained an extra 10Mb/s of inflation rate. The blit function is the most important function when it comes to inflating the window to an output flow. As the specialization on the min function, this is one of the biggest optimization on decompress.

hot-loop

A common design about decompression (but we can find it on hash implementation too), is the hot-loop. An hot-loop is mainly a loop on the most common operation in your process. In the context of decompress, the hot-loop is about a repeated translation from bits-sequence to byte(s) from the inputs flow to the outputs flow and the window.

The main idea behind the hot-loop is to initialize all information needed for the translation before to start the hot-loop. Then, it's mostly an imperative loop with a pattern-matching which corresponds to the current state of the global computation.

In OCaml, we can take this opportunity to use int ref (or nativeint ref), and then, they will be translated into registers (which is the fastest area to store something).

Another deal inside the hot-loop is to avoid any allocation – and it's why we talk about int or nativeint. Indeed, a more complex structure like an option will add a blocker to the garbage collection (a call to caml_call_gc).

Of course, this kind of design is completely wrong if we think in a functional way. However, this is the (biggest?) advantage of OCaml: hide this ugly/hacky part inside a functional interface.

In the API, we talked about a state which represents the inflation (or the deflation). At the beginning, the goal is to store into some references essentials values like the position into the inputs flow, bits available, dictionary, etc. Then, we launch the hot-loop and only at the end, we update the state.

So we keep the optimal design about inflation and the functional way outside the hot-loop.

caml_modify

One issue that we need to consider is the call to caml_modify. In fact, for a complex data-structure like an int array or a int option (so, other than an integer or a boolean or an immediate value), values can move to the major heap.

In this context, caml_modify is used to assign a new value into your mutable block. It is a bit slower than a simple assignment but needed to ensure pointer correspondence between minor heap and major heap.

With this OCaml code for example:

type t = { mutable v : int option }

let f t v = t.v <- v

We produce this assembly:

camlExample__f_1004:
        subq    $8, %rsp
        movq    %rax, %rdi
        movq    %rbx, %rsi
        call    caml_modify@PLT
        movq    $1, %rax
        addq    $8, %rsp
        ret

Where we see the call to caml_modify which will be take care about the assignment of v into t.v. This call is needed mostly because the type of t.v is not an immediate value like an integer. So, for many values in the inflator and the deflator, we mostly use integers.

Of course, at some points, we use int array and set them at some specific points of the inflator – where we inflated the dictionary. However, the impact of caml_modify is not very clear where it is commonly pretty fast.

Sometimes, however, it can be a real bottleneck in your computation and this depends on how long your values live in the heap. A little program (which is not very reproducible) can show that:

let t = Array.init (int_of_string Sys.argv.(1)) (fun _ -> Random.int 256)

let pr fmt = Format.printf fmt

type t0 = { mutable v : int option }
type t1 = { v : int option }

let f0 (t0 : t0) =
  for i = 0 to Array.length t – 1
  do let v = match t0.v, t.(i) with
             | Some _ as v, _ -> v
             | None, 5 -> Some i
             | None, _ -> None in
     t0.v <- v
  done; t0

let f1 (t1 : t1) =
  let t1 = ref t1 in
  for i = 0 to Array.length t – 1
  do let v = match !t1.v, t.(i) with
             | Some _ as v, _ -> v
             | None, 5 -> Some i
             | None, _ -> None in
     t1 := { v }
  done; !t1

let () =
  let t0 : t0 = { v= None } in
  let t1 : t1 = { v= None } in
  let time0 = Unix.gettimeofday () in
  ignore (f0 t0) ;
  let time1 = Unix.gettimeofday () in
  ignore (f1 t1) ;
  let time2 = Unix.gettimeofday () in

  pr "f0: %f ns\n%!" (time1 -. time0) ;
  pr "f1: %f ns\n%!" (time2 -. time1) ;

  ()

In our bare-metal server, if you launch the program with 1000, the f0 computation, even if it has caml_modify will be the fastest. However, if you launch the program with 1000000000, f1 will be the fastest.

$ ./a.out 1000
f0: 0.000006 ns
f1: 0.000015 ns
$ ./a.out 1000000000
f0: 7.931782 ns
f1: 5.719370 ns

About `decompress`

At the beginning, our choice was made to have, as @dbuenzli does, mutable structure to represent state. Then, @yallop did a big patch to update it to an immutable state and we won 9Mb/s on inflation.

However, the new version is more focused on the hot-loop and it is 3 times faster than before.

As we said, the deal about caml_modify is not clear and depends a lot about how long your data lives in the heap and how many times you want to update it. If we localize caml_modify only on few places, it should be fine. But it still is one of the most complex question about (macro?) optimization.

Smaller representation

We've discussed the impact that integer types can have on the use of immediate values. More generally, the choice of type to represent your values can have significant performance implications.

For example, a dictionary which associates a bits-sequence (an integer) to the length of it AND the byte, it can be represented by a: (int * int) array, or more idiomatically { len: int; byte: int; } array (which is structurally the same).

However, that means an allocation for each bytes to represent every bytes. Extraction of it will need an allocation if find : bits:int -> { len: int; byte: int; } is not inlined as we said. And about memory, the array can be really heavy in your heap.

At this point, we used spacetime to show how many blocks we allocated for a common inflation and we saw that we allocate a lot. The choice was made to use a smaller representation. Where len can not be upper than 15 according RFC 1951 and when byte can represent only 256 possibilities (and should fit under one byte), we can decide to merge them into one integer (which can have, at least, 31 bits).

let static_literal_tree = [| (8, 12); (8, 140); (8, 76); ... |]
let static_literal_tree = Array.map (fun (len, byte) -> (len lsl 8) lor byte) static_literal_tree

In the code above, we just translate the static dictionary (for a STATIC DEFLATE block) to a smaller representation where len will be the left part of the integer and byte will be the right part. Of course, it's depends on what you want to store.

Another point is readability. `cstruct-ppx` and `bitstring` can help you but decompress wants to depend only on OCaml.

Conclusion

We conclude with some closing advice about optimising your OCaml programs:

Optimization is specific to your task. The points highlighted in this article may not fit your particular problem, but they are intended to give you ideas. Our optimizations were only possible because we completely assimilated the ideas of zlib and had a clear vision of what we really needed to optimize (like blit).

As your first project, this article can not help you a lot to optimize your code where it's mostly about micro-optimization under a specific context (hot-loop). But it helps you to understand what is really done by the compiler – which is still really interesting.
Optimise only with respect to an oracle. All optimizations were done because we did a comparison point between the old implementation of decompress and zlib as oracles. Optimizations can change the semantics of your code and you should systematically take care at any step about expected behaviors. So it's a long run.
Use the predictability of the OCaml compiler to your advantage. For sure, the compiler does not optimize a lot your code – but it sill produce realistic programs if we think about performance. For many cases, you don't need to optimize your OCaml code. And the good point is about expected behavior.

The mind-link between the OCaml and the assembly exists (much more than the C and the assembly sometimes where we let the C compiler to optimize the code). The cool fact is to keep a mental-model about what is going on on your code easily without to be afraid by what the compiler can produce. And, in some critical parts like eqaf, it's really needed.

We have not discussed benchmarking, which is another hard issue: who should you compare with? where? how? For example, a global comparison between zlib and decompress is not very relevant in many ways – especially because of the garbage collector. This could be another article!

Finally, all of these optimizations should be done by flambda; the difference between compiling decompress with or without flambda is not very big. We optimized decompress by hand mostly to keep compatibility with OCaml (since flambda needs another switch) and, in this way, to gain an understanding of flambda optimizations so that we can use it effectively!

Hide

On complete ordered fields — Andrej Bauer, Sep 08, 2019

Joel Hamkins advertised the following theorem on Twitter:

Theorem: All complete ordered fields are isomorphic.

The standard proof posted by Joel has two parts:

A complete ordered field is archimedean.
Using the fact that the rationals are dense in an archimedean field, we construct an isomorphism between any two complete ordered fields.

The second step is constructive, but the first one is proved using excluded middle, as follows. Suppose $F$ is a complete ordered field. If $b \in …

Joel Hamkins advertised the following theorem on Twitter:

Theorem: All complete ordered fields are isomorphic.

The standard proof posted by Joel has two parts:

A complete ordered field is archimedean.
Using the fact that the rationals are dense in an archimedean field, we construct an isomorphism between any two complete ordered fields.

The second step is constructive, but the first one is proved using excluded middle, as follows. Suppose $F$ is a complete ordered field. If $b \in F$ is an upper bound for the natural numbers, construed as a subset of $F$, then so $b - 1$, but then no element of $F$ can be the least upper bound of $\mathbb{N}$. By excluded middle, above every $x \in F$ there is $n \in \mathbb{N}$.

So I asked myself and the constructive news mailing list what the constructive status of the theorem is. But something was amiss, as Fred Richman immediately asked me to provide an example of a complete ordered field. Why would he do that, don't we have the MacNeille reals? After agreeing on definitions, Toby Bartels gave the answer, which I am taking the liberty to adapt a bit and present here. I am probably just reinventing the wheel, so if someone knows an original reference, please provide it in the comments.

The theorem holds constructively, but for a bizarre reason: if there exists a complete ordered field, then the law of excluded middle holds, and the standard proof is valid!

As there are many constructive versions of order and completeness, let me spell out the definitions that are well adapted to the oddities of constructive mathematics. In classical logic these are all equivalent to the usual ones. Having to disentangle definitions when passing to constructive mathematics is a bit like learning how to be careful when passing from commutative to non-commutative algebra.

A partial order $\leq$ on a set $P$ is a reflexive, transitive and antisymmetric relation on $P$.

We are interested in linearly ordered fields, but constructively we need to take care, as the usual linearity, $x \leq y \lor y \leq x$, is quite difficult to satisfy, and may fail for reals.

A strict order on a set $P$ is a relation $<$ which is:

irreflexive: $\lnot (x < x)$,
tight: $\lnot (x < y \lor y < x) \Rightarrow x = y$,
weakly linear: $x < y \Rightarrow x < z \lor z < y$

The associated partial order is defined by $x \leq y \Leftrightarrow \lnot (y < x)$. The reflexivity, antisymmetry and transitivity of $\leq$ follow respectively from irreflexivity, tightness, and weak linearity of $<$.

Next, an element $x \in P$ is an upper bound for $S \subseteq P$ when $y \leq x$ for all $y \in P$. An element $x \in P$ is the supremum of $S \subseteq P$ if it is an upper bound for $S$, and for every $y < x$ there exists $z \in S$ such that $y < z$. A poset $P$ is (Dedekind-MacNeille) complete when every inhabited bounded subset has a supremum (for the classically trained, $S \subseteq P$ is inhabited when there exists $x \in S$, and this is not the same as $S \neq \emptyset$).

A basic exercise is to give a non-trivial complete order, i.e., a strict order $<$ whose associated partial order $\leq$ is complete.

Theorem: If there exists a non-trivial complete order then excluded middle holds.

Proof. Suppose $<$ is a strict order on a set $P$ whose associated order $\leq$ is complete, and there exist $a, b \in P$ such that $a < b$. Let $\phi$ be any proposition. Consider the set $S = \lbrace x \in P \mid x = a \lor (\phi \land x = b)\rbrace$. Observe that $\phi$ is equivalent to $b \in S$. Because $a \in S \subseteq \lbrace a, b\rbrace$, the set $S$ is inhabited and bounded, so let $s$ be its supremum. We know that $a < s$ or $s < b$, from which we can decide $\phi$:

If $a < s$ then $b \in S$: indeed, there exists $c \in S$ such that $a < c$, but then $c = b$. In this case $\phi$ holds.
If $s < b$ then $\lnot(b \in S)$: if we had $b \in S$ then $S = \lbrace a, b \rbrace$ and $b = s < b$, which is impossible. In this case $\lnot\phi$. $\Box$

This immediately gives us the desired theorem.

Theorem (constructive): All complete ordered fields are isomorphic.

Proof. The definition of a complete ordered field requires $0 < 1$, therefore excluded middle holds. Now proceed with the usual classical proof. $\Box$

This is very odd, as I always thought that the MacNeille reals form a MacNeille complete ordered field. Recall that a MacNeille real is a pair $(L, U)$ of subsets of $\mathbb{Q}$ such that:

$U$ is the set of upper bounds of $L$: $u \in U$ if, and only if, $\ell \leq u$ for all $\ell \in L$,
$L$ is the set of lower bounds of $U$: $\ell \in L$ if, and only if, $\ell \leq u$ for all $u \in U$,
$L$ and $U$ are inhabited.

Furthermore, the MacNeille reals are complete, as they are just the MacNeille completion of the rationals. We may define a strict order on them by stipulating that, for $x = (L_x, U_x)$ and $y = (L_y, U_y)$, $$x < y \iff \exists q \in U_x . \exists r \in L_y \,.\, q < r.$$ According to Peter Johnstone (Sketches of an Elephant, D4.7), the MacNeille reals form a commutative unital ring in which $x$ is invertible if, and only if, $x < 0 \lor x > 0$. So apparently, the weak linearity of the strict order is problematic.

What if we relax completeness? Two standard notions of completeness are:

An ordered field $F$ is Cauchy-complete if every Cauchy sequence has a limit in $F$.
An ordered field $F$ is Dedekind-complete if every Dedekind cut determines an element of $F$.

It is easy enough to find non-isomorphic Cauchy-complete fields. Order the field $\mathbb{Q}(x)$ of rational functions with rational coefficients by stipulating that it extends the order of $\mathbb{Q}$ and that $q < x$ for all $q \in \mathbb{Q}$. The Cauchy-completion of $\mathbb{Q}(x)$ is a Cauchy complete field which is not isomorphic to $\mathbb{Q}$. Caveat: I am speaking off the top of my head, do not trust this paragraph! (Or any other for that matter.)

Regarding Dedekind completeness, it is important constructively that we take two-sided Dedekind cuts, i.e., pairs $(L, U)$ of subsets of $F$ such that

$L$ is lower-rounded: $q \in L \iff \exists r \in L . q < r$,
$U$ is upper-rounded: $r \in U \iff \exists q \in U . q < r$,
the cut is bounded: $L$ and $U$ are inhabited,
the cut is disjoint: $L \cap U = \emptyset$,
the cut is located: if $q < r$ then $L \in q$ or $r \in U$.

Dedekind completeness states that for every Dedekind cut $(L, U)$ in $F$ there exists a unique $x \in F$ such that $L = \lbrace y \in F \mid y < x\rbrace$ and $U = \lbrace y \in F \mid x < y\rbrace$. Constructively this is a weaker form of completeness than the Dedekind-MacNeille one, but classically they coincide. Thus we cannot hope to exhibit constructively two non-isomorphic Dedekind-complete ordered fields (because constructive results are also classically valid). But perhaps there is a model of constructive mathematics where such strange fields exist. Does anyone know of one?

Hide

An introduction to fuzzing OCaml with AFL, Crowbar and Bun — Tarides (Nathan Rebours), Sep 04, 2019

American Fuzzy Lop or AFL is a fuzzer: a program that tries to find bugs in other programs by sending them various auto-generated inputs. This article covers the basics of AFL and shows an example of fuzzing a parser written in OCaml. It also introduces two extensions: the Crowbar library which can be used to fuzz any kind of OCaml program or function and the Bun tool for integrating fuzzing into your CI.

All of the examples given in this article are available on GitHub at ocaml-afl-examples. Th…

All of the examples given in this article are available on GitHub at ocaml-afl-examples. The README contains all the information you need to understand, build and fuzz them yourself.

What is AFL?

AFL actually isn't just a fuzzer but a set of tools. What makes it so good is that it doesn't just blindly send random input to your program hoping for it to crash; it inspects the execution paths of the program and uses that information to figure out which mutations to apply to the previous inputs to trigger new execution paths. This approach allows for much more efficient and reliable fuzzing (as it will try to maximize coverage) but requires the binaries to be instrumented so the execution can be monitored.

AFL provides wrappers for the common C compilers that you can use to produce the instrumented binaries along with the CLI fuzzing client: afl-fuzz.

afl-fuzz is straight-forward to use. It takes an input directory containing a few initial valid inputs to your program, an output directory and the instrumented binary. It will then repeatedly mutate the inputs and feed them to the program, registering the ones that lead to crashes or hangs in the output directory.

Because it works in such a way, it makes it very easy to fuzz a parser.

To fuzz a parse.exe binary, that takes a file as its first command-line argument and parses it, you can invoke afl-fuzz in the following way:

$ afl-fuzz -i inputs/ -o findings/ /path/to/parse.exe @@

The findings/ directory is where afl-fuzz will write the crashes it finds, it will create it for you if it doesn't exist. The inputs/ directory contains one or more valid input files for your program. By valid we mean "that don't crash your program". Finally the @@ part tells afl-fuzz where on the command line the input file should be passed to your program, in our case, as the first argument.

Note that it is possible to supply afl-fuzz with more detail about how to invoke your program. If you need to pass it command-line options for instance, you can run it as:

$ afl-fuzz -i inputs/ -o findings/ -- /path/to/parse.exe --option=value @@

If you wish to fuzz a program that takes its input from standard input, you can also do that by removing the @@ from the afl-fuzz invocation.

Once afl-fuzz starts, it will draw a fancy looking table on the standard output to keep you updated about its progress. From there, you'll mostly be interested in is the top right corner which contains the number of crashes and hangs it has found so far:

Example output from afl-fuzz

You might need to change some of your CPU settings to achieve better performance while fuzzing. afl-fuzz's output will tell you if that's the case and guide you through the steps required to make that happen.

Using AFL to fuzz an OCaml parser

First of all, if you want to fuzz an OCaml program with AFL you'll need to produce an instrumented binary. afl-fuzz has an option to work with regular binaries but you'd lose a lot of what makes it efficient. To instrument your binary you can simply install a +afl opam switch and build your executable from there. AFL compiler variants are available from OCaml 4.05.0 onwards. To install such a switch you can run:

$ opam switch create fuzzing-switch 4.07.1+afl

If your program already parses the standard input or a file given to it via the command line, you can simply build the executable from your +afl switch and adapt the above examples. If it doesn't, it's still easy to fuzz any parsing function.

Imagine we have a simple-parser library which exposes the following parse_int function:

val parse_int: string -> (int, [> `Msg of string]) result
(** Parse the given string as an int or return [Error (`Msg _)].
    Does not raise, usually... *)

We want to use AFL to make sure our function is robust and won't crash when receiving unexpected inputs. As you can see the function returns a result and isn't supposed to raise exceptions. We want to make sure that's true.

To find crashes, AFL traps the signals sent by your program. That means that it will consider uncaught OCaml exceptions as crashes. That's good because it makes it really simple to write a fuzz_me.ml executable that fits what afl-fuzz expects:

let () =
  let file = Sys.argv.(1) in
  let ic = open_in file in
  let length = in_channel_length ic in
  let content = really_input_string ic length in
  close_in ic;
  ignore (Simple_parser.parse_int content)

We have to provide example inputs to AFL so we can write a valid file to the inputs/ directory containing 123 and an invalid file containing not an int. Both should parse without crashing and make good starting point for AFL as they should trigger different execution paths.

Because we want to make sure AFL does find crashes we can try to hide a bug in our function:

let parse_int s =
  match List.init (String.length s) (String.get s) with
  | ['a'; 'b'; 'c'] -> failwith "secret crash"
  | _ -> (
      match int_of_string_opt s with
      | None -> Error (`Msg (Printf.sprintf "Not an int: %S" s))
      | Some i -> Ok i)

Now we just have to build our native binary from the right switch and let afl-fuzz do the rest:

$ afl-fuzz -i inputs/ -o findings/ ./fuzz_me.exe @@

It should find that the abc input leads to a crash rather quickly. Once it does, you'll see it in the top right corner of its output as shown in the picture from the previous section.

At this point you can interrupt afl-fuzz and have a look at the content of the findings/crashes:

$ ls findings/crashes/
id:000000,sig:06,src:000111,op:havoc,rep:16  README.txt

As you can see it contains a README.txt which will give you some details about the afl-fuzz invocation used to find the crashes and how to reproduce them in the folder and a file of the form id:...,sig:...,src:...,op:...,rep:... per crash it found. Here there's just one:

$ cat findings/crashes/id:000000,sig:06,src:000111,op:havoc,rep:16
abc

As expected it contains our special input that triggers our secret crash. We can rerun the program with that input ourselves to make sure it does trigger it:

$ ./fuzz_me.exe findings/crashes/id:000000,sig:06,src:000111,op:havoc,rep:16
Fatal error: exception Failure("secret crash")

No surprise here, it does trigger our uncaught exception and crashes shamefully.

Using Crowbar and AFL for property-based testing

This works well but only being able to fuzz parsers is quite a limitation. That's where Crowbar comes into play.

Crowbar is a property-based testing framework. It's much like Haskell's QuickCheck. To test a given function, you define how its arguments are shaped, a set of properties the result should satisfy and it will make sure they hold with any combinations of randomly generated arguments. Let's clarify that with an example.

I wrote a library called Awesome_list and I want to test its sort function:

val sort: int list -> int list
(** Sorts the given list of integers. Result list is sorted in increasing
    order, most of the time... *)

I want to make sure it really works so I'm going to use Crowbar to generate a whole lot of lists of integers and verify that when I sort them with Awesome_list.sort the result is, well... sorted.

We'll write our tests in a fuzz_me.ml file. First we need to tell Crowbar how to generate arguments for our function. It exposes some combinators to help you do that:

let int_list = Crowbar.(list (range 10))

Here we're telling Crowbar to generate lists of any size, containing integers ranging from 0 to 10. Crowbar also exposes more complex and custom generator combinators so don't worry, you can use it to build more complex arguments.

Now we need to define our property. Once again it's pretty simple, we just want the output to be sorted:

let is_sorted l =
  let rec is_sorted = function
    | [] | [_] -> true
    | hd::(hd'::_ as tl) -> hd <= hd' && is_sorted tl
  in
  Crowbar.check (is_sorted l)

All that's left to do now is to register our test:

let () =
  Crowbar.add_test ~name:"Awesome_list.sort" [int_list]
      (fun l -> is_sorted (Awesome_list.sort l))

and to compile that fuzz_me.ml file to a binary. Crowbar will take care of the magic.

We can run that binary in "Quickcheck" mode where it will either try a certain amount of random inputs or keep trying until one of the properties breaks depending on the command-line options we pass it. What we're interested in here is its less common "AFL" mode. Crowbar made it so our executable can be used with afl-fuzz just like that:

$ afl-fuzz -i inputs -o findings -- ./fuzz_me.exe @@

What will happen then is that our fuzz_me.exe binary will read the inputs provided by afl-fuzz and use it to determine which test to run and how to generate the arguments to pass to our function. If the properties are satisfied, the binary will exit normally; if they aren't, it will make sure that afl-fuzz interprets that as a crash by raising an exception.

A nice side-effect of Crowbar's approach is that afl-fuzz will still be able to pick up crashes. For instance, if we implement Awesome_list.sort as:

let sort = function
  | [1; 2; 3] -> failwith "secret crash"
  | [4; 5; 6] -> [6; 5; 4]
  | l -> List.sort Pervasives.compare l

and use AFL and Crowbar to fuzz-test our function, it will find two crashes: one for the input [1; 2; 3] which triggers a crash and one for [4; 5; 6] for which the is_sorted property won't hold.

The content of the input files found by afl-fuzz itself won't be of much help as it needs to be interpreted by Crowbar to build the arguments that were passed to the function to trigger the bug. We can invoke the fuzz_me.exe binary ourselves on one of the files in findings/crashes and the Crowbar binary will replay the test and give us some more helpful information about what exactly is going on:

$ ./fuzz_me.exe findings/crashes/id\:000000\,sig\:06\,src\:000011\,op\:flip1\,pos\:5 
Awesome_list.sort: ....
Awesome_list.sort: FAIL

When given the input:

    [1; 2; 3]
    
the test threw an exception:

    Failure("secret crash")
    Raised at file "stdlib.ml", line 33, characters 17-33
    Called from file "awesome-list/fuzz/fuzz_me.ml", line 11, characters 78-99
    Called from file "src/crowbar.ml", line 264, characters 16-19
    
Fatal error: exception Crowbar.TestFailure
$ ./fuzz_me.exe findings/crashes/id\:000001\,sig\:06\,src\:000027\,op\:arith16\,pos\:5\,val\:+7 
Awesome_list.sort: ....
Awesome_list.sort: FAIL

When given the input:

    [4; 5; 6]
    
the test failed:

    check false
    
Fatal error: exception Crowbar.TestFailure

We can see the actual inputs as well as distinguish the one that broke the invariant from the one that triggered a crash.

Using `bun` to run fuzz testing in CI

While AFL and Crowbar provide no guarantees they can give you confidence that your implementation is not broken. Now that you know how to use them, a natural follow-up is to want to run fuzz tests in your CI to enforce that level of confidence.

Problem is, AFL isn't very CI friendly. First it has this refreshing output that isn't going to look great on your travis builds output and it doesn't tell you much besides that it could or couldn't find crashes or invariant infrigements

Hopefully, like most problems, this one has a solution: `bun`. bun is a CLI wrapper around afl-fuzz, written in OCaml, that helps you get the best out of AFL effortlessly. It mostly does two things:

The first is that it will run several afl-fuzz processes in parallel (one per core by default). afl-fuzz starts with a bunch of deterministic steps. In my experience, using parallel processes during this phase rarely proved very useful as they tend to find the same bugs or slight variations of those bugs. It only achieves its full potential in the second phase of fuzzing.

The second thing, which is the one we're the most interested in, is that bun provides a useful and CI-friendly summary of what's going on with all the fuzzing processes so far. When one of them finds a crash, it will stop all processes and pretty-print all of the bug-triggering inputs to help you reproduce and debug them locally. See an example bun output after a crash was found:

Crashes found! Take a look; copy/paste to save for reproduction:
1432    echo JXJpaWl0IA== | base64 -d > crash_0.$(date -u +%s)
1433    echo NXJhkV8QAA== | base64 -d > crash_1.$(date -u +%s)
1434    echo J3Jh//9qdGFiYmkg | base64 -d > crash_2.$(date -u +%s)
1435    09:35.32:[ERROR]All fuzzers finished, but some crashes were found!

Using bun is very similar to using afl-fuzz. Going back to our first parser example, we can fuzz it with bun like this:

$ bun --input inputs/ --output findings/ /path/to/parse.exe

You'll note that you don't need to provide the @@ anymore. bun assumes that it should pass the input as the first argument of your to-be-fuzzed binary.

bun also comes with an alternative no-kill mode which lets all the fuzzers run indefinitely instead of terminating them whenever a crash is discovered. It will regularly keep you updated on the number of crashes discovered so far and when terminated will pretty-print each of them just like it does in regular mode.

This mode can be convenient if you suspect your implementation may contain a lot of bugs and you don't want to go through the whole process of fuzz testing it to only find a single bug.

You can use it in CI by running bun --no-kill via timeout. For instance:

timeout --preserve-status 60m bun --no-kill --input inputs --output findings ./fuzz_me.exe

will fuzz fuzz_me.exe for an hour no matter what happens. When timeout terminates bun, it will provide you with a handful of bugs to fix!

Final words

I really want to encourage you to use those tools and fuzzing in general. Crowbar and bun are fairly new so you will probably encounter bugs or find that it lacks a feature you want but combined with AFL they make for very nice tools to effectively test critical components of your OCaml code base or infrastructure and detect newly-introduced bugs. They are already used accross the MirageOS ecosystem where it has been used to fuzz the TCP/IP stack mirage-tcpip and the DHCP implementation charrua thanks to somerandompacket. You can consult Crowbar's hall of fame to find out about bugs uncovered by this approach.

I also encourage anyone interested to join us in using this promising toolchain, report those bugs, contribute those extra features and help the community build more robust software.

Finally if you wish to learn more about how to efficienly use fuzzing for testing I recommend the excellent Write Fuzzable Code article by John Regehr.

Hide

What is algebraic about algebraic effects? — Andrej Bauer, Sep 02, 2019

Published as arXiv:1807.05923.

Abstract: This note recapitulates and expands the contents of a tutorial on the mathematical theory of algebraic effects and handlers which I gave at the Dagstuhl seminar 18172 "Algebraic effect handlers go mainstream". It is targeted roughly at the level of a doctoral student with some amount of mathematical training, or at anyone already familiar with algebraic effects and handlers as programming concepts who would like to know what they have to do with algebra.…

The blog moved from Wordpress to Jekyll — Andrej Bauer, Sep 02, 2019

You may have noticed that lately I have had trouble with the blog. It was dying periodically because the backend database kept crashing. It was high time I moved away from Wordpress anyway, so I bit the bullet and ported the blog.

All in all, it was a typical system administration experience: lots of installing Ruby and Node.js packages, figuring out which of several equivalent tools actually is worth using, dealing with scarce and obsolete documentation (a blog post is not a good substitute …

OCamlPro’s compiler team work update — OCamlPro, Aug 30, 2019

The OCaml compiler team at OCamlPro is happy to present some of the work recently done jointly with JaneStreet’s team.

A lot of work has been done towards a new framework for optimizations in the compiler, called Flambda2, aiming at solving the shortcomings that became apparent in the Flambda optimization framework (see below for more details). While that work is in progress, the team also worked on some more short-term improvements, notably on the current Flambda optimization framework, a…

The OCaml compiler team at OCamlPro is happy to present some of the work recently done jointly with JaneStreet’s team.

This work is funded by JaneStreet

Short-term improvements

Recursive values compilation

OCaml supports quite a large range of recursive definitions. In addition to recursive (and mutually-recursive) functions, one can also define regular values recursively, as for the infinite list let rec l = 0 :: l.

Not all recursive constructions are allowed, of course. For instance, the definition let rec x = x is rejected because there is no way to actually build a value that would behave correctly.

The basic rule for deciding whether a definition is allowed or not is made under the assumption that recursive values (except for functions, mostly) are compiled by first allocating space in the heap for the recursive values, binding the recursively defined variables to the allocated (but not yet initialized) values. The defining expressions are then evaluated, yielding new values (that can contain references the non-initialized values). Finally, the fields of these new values are copied one-by-one into the corresponding fields of the initial values.

For this approach to work, some restrictions need to apply:

the compiler needs to be able to compute the size of the values beforehand (these values must be allocated values, in order to avoid defining an integer recursively),
and since during the evaluation of the defining expressions their fields are not valid, one cannot write any code that may read these fields, like pattern-matching on the value, or passing the value to some function (or storing it in a mutable field of some record).

All of those restrictions have recently been reworked and formalized based on work from Alban Reynaud during an internship at Inria, reviewed and completed by Gabriel Scherer and Jeremy Yallop.

Unfortunately, this work only covers checking whether the recursive definitions are allowed or not; actual compilation is done later in the compiler, in one place for bytecode and another for native code, and these pieces of code have not been linked with the new check so there have been a few cases where the check allowed code that wasn’t actually compiled correctly.

Since we didn’t want to deal with it directly in our new version of Flambda, we had started working on a patch to move the compilation of recursive values up in the compilation pipeline, before the split between bytecode and native code. After some amount of hacking (we discovered that compilation of classes creates recursive value bindings that would not pass the earlier recursive check…), we have a patch that is mostly ready for review and will soon start engaging with the rest of the compiler team with the aim of integrating it into the compiler.

Separate compilation of recursive modules, compilation units as functors

Some OCaml developers like to encapsulate each type definition in its own module, with an interface that can expose the needed types and functions, while abstracting away as much of the actual implementation as possible. It is then common to have each of these modules in its own file, to simplify management and avoid unseemly big files.

However, this breaks down when one needs to define several types that depend on each other. The usual solutions are either to use recursive modules, which have the drawback of requiring all the modules to be in the same compilation unit, leading to very big files (we have seen a real case of a more than 10,000-lines file), or make each module parametric in the other modules, translating them into functors, and then instantiate all the functors when building the outwards-facing interface.

To address these issues, we have been working on two main patches to improve the life of developers facing these problems.

The first one allows compiling several different files as mutually recursive modules, reusing the approach used to compile regular recursive modules. In practice, this will allow developers using recursive modules extensively to properly separate not only the different modules from each other, but also the implementation and interfaces into a .ml and .mli files. This would of course need some additional support from the different build tools, but we’re confident we can get at least dune to support the feature.

The second one allows compiling a single compilation unit as a functor instead of a regular module. The arguments of the functor would be specified on the command line, their signature taken from their corresponding interface file. This can be useful not only to break recursive dependencies, like the previous patch (though in a different way), but also to help developers relying on multiple implementations of a same .mli interface functorize their code with minimal effort.

These two improvements will also benefit packs, whereas recursive compilation units could be packed in a single module and packs could be functorized themselves.

Small improvements to Flambda

We are still committed to maintain the Flambda part of the compiler. Few bugs have been found, so we concentrate our efforts on small features that either yield overall performance gains or allow naive code patterns to be compiled as efficiently as their equivalent but hand-optimized versions.

As an example, one optimization that we should be able to submit soon looks for cases where an immutable block is allocated but an immutable block with the same exact fields and tag already exists.

This can be demonstrated with the following example:

let result_bind f = function
  | Ok x -> f x
  | Error e -> Error e

The usual way to avoid the extra allocation of Error e is to write the clause as | (Error e) as r -> r. With this new patch, the redundant allocation will be detected and removed automatically! This can be even more interesting with inlining:

let my_f x =
  if (* some condition *)
  then Ok x
  else (* something else *)

let _ =
  (* ... *)
  let r = result_bind my_f (* some argument *) in
  (* ... *)

In this example, inlining result_bind then my_f can match the allocation Ok x in my_f with the pattern matching in result_bind. This removes an allocation that would be very hard to remove otherwise. We expect these patterns to occur quite often with some programming styles relying on a great deal of abstraction and small independent functions.

Flambda 2.0

We are building on the work done for Flambda and the experience of its users to develop Flambda 2.0, the next optimization framework.

Our goal is to build a framework for analyzing the costs and benefits of code transformations. The framework focuses on reducing the runtime cost of abstractions and removing as many short-lived allocations as possible.

The aim of Flambda 2.0 is roughly the same as the original Flambda. So why did we decide to write a new framework instead of patching the existing one? Several points led us to this decision.

An invariant on the representation of closures that ensured that every closure had a unique identifier, which was convenient for a number of reasons, turned out to be quite expensive to maintain and prevented some optimizations.
The internal representation of Flambda terms included too many different cases that were either redundant or not relevant to the optimizations we were interested in, making a lot of code more complicated than necessary.
The ANF-like representation we used was not perfect. We wanted an easier way to do control flow optimizations, which led us to choose a CPS-like representation for Flambda 2.0.
Finally, the original Flambda was thought of as an alternative to the closure conversion and inlining algorithms performed by the Closure module of the compiler, translating from the Lambda representation to Clambda. However, a number of optimizations (most importantly unboxing) are done during the next phase of compilation, Cmmgen, which translates to the Cmm representation. The original Flambda had trouble to estimate correctly which optimizations would trigger and what would their benefit be. It may be noted that correctly estimating benefit is a key in Flambda’s algorithms, and we know of a number of cases where Flambda is not as good as it could be because it couldn’t predict the unboxing opportunities that inlining would have allowed. Flambda 2.0 will go from Lambda to Cmm, and will handle all transformations done in both Closure and Cmmgen in a single framework.

These improvements are still very much a work in progress. We have not reached the point where other developers can try out the new framework on their codebases yet.

This does not mean there are no news to enjoy before our efforts show on the mainstream compiler! While working on Flambda 2.0, we did deploy a number of patches on the compiler both before and after the Flambda stage. We proposed all the changes independant enough to be proposed on their own. Some of these fixes have been merged already. Others are still under discussion and some, like the recursive values patch mentioned above, are still waiting for cleanup or documentation before submission.

Hide

What the interns have wrought, 2019 edition — Jane Street, Aug 30, 2019

Jane Street’s intern program yet again is coming to an end, which is a nice opportunity to look back over the summer and see what they’ve accomplished.

Decompress: The New Decompress API — Tarides (Romain Calascibetta), Aug 26, 2019

RFC 1951 is one of the most used standards. Indeed, when you launch your Linux kernel, it inflates itself according zlib standard, a superset of RFC 1951. Being a widely-used standard, we decided to produce an OCaml implementation. In the process, we learned many lessons about developing OCaml where we would normally use C. So, we are glad to present `decompress`.

One of the many users of RFC 1951 is Git, which uses it to pack data objects into a PACK file. At the request of @samoht, decompress …

One of the many users of RFC 1951 is Git, which uses it to pack data objects into a PACK file. At the request of @samoht, decompress appeared some years ago as a Mirage-compatible replacement for zlib to be used for compiling a MirageOS unikernel with ocaml-git. Today, this little project passes a major release with substantial improvements in several domains.

decompress provides an API for inflating and deflating flows[1]. The main goal is to provide a platform-agnostic library: one which may be compiled on any platform, including JavaScript. We surely cannot be faster than C implementations like zstd or lz4, but we can play some optimisation tricks to help bridge the gap. Additionally, OCaml can protect the user against lot of bugs via the type-system and the runtime too (e.g. using array bounds checking). `ocaml-tls` was implemented partly in response to the famous failure of openssl; a vulnerability which could not exist in OCaml.

[1]: A flow, in MirageOS land, is an abstraction which wants to receive and/or transmit something under a standard. So it's usual to say a TLS-flow for example.

API design

The API should be the most difficult part of designing a library - it reveals what we can do and how we should do it. In this way, an API should:

constrain the user to avoid security issues; too much freedom can be a bad thing. As an example, consider the Hashtbl.create function, which allows the user to pass ~random:false to select a fixed hash function. The resulting hashtable suffers deterministic key collisions, which can be exploited by an attacker.

An example of good security-awareness in API design can be seen in digestif, which provided an unsafe_compare instead of the common compare function (before eqaf.0.5). In this way, it enforced the user to create an alias of it if they want to use a hash in a Map – however, by this action, they should know that they are not protected against a timing-attack.
allow some degrees of freedom to fit within many environments; a constrained API cannot support a hostile context. For example, when compiling to an ESP32 target, even small details such as the length of a stream input buffer must be user-definable. When deploying to a server, memory consumption should be deterministic.

Of course, this is made difficult when too much freedom will enable misuse of the API – an example is dune which wants consciously to limit the user about what they can do with it.
imply an optimal design of how to use it. Possibilities should serve the user, but these can make the API harder to understand; this is why documentation is important. Your API should tell your users how it wants to be treated.

A dbuenzli API

From our experiences with protocol/format, one design stands out: the dbuenzli API. If you look into some famous libraries in the OCaml eco-system, you probably know uutf, jsonm or xmlm. All of these libraries provide the same API for computing a Unicode/JSON/XML flow – of course, the details are not the same.

From a MirageOS perspective, even if they use the in_channel/out_channel abstraction rather than a Mirage flow, these libraries are system-agnostic since they let the user to choose input and output buffers. Most importantly, they don't use the standard OCaml Unix module, which cannot be used in a unikernel.

The APIs are pretty consistent and try to do their best-effort[2] of decoding. The design has a type state which represents the current system status; the user passes this to decode/encode to carry out the processing. Of course, these functions have a side-effect on the state internally, but this is hidden from the user. One advantage of including states in a design is that the underlying implementation is very amenable to compiler optimisations (e.g. tail-call optimisation). Internally, of course, we have a porcelain[3] implementation where any details can have an rational explanation.

In the beginning, decompress wanted to follow the same interface without the mutability (a choice about performances) and it did. Then, the hard test was to use it in a bigger project; in this case, ocaml-git. An iterative process was used to determine what was really needed, what we should not provide (like special cases) and what we should provide to reach an uniform API that is not too difficult to understand.

From this experience, we finalised the initial decompress API and it did not change significantly for 4 versions (2 years).

[2]: best-effort means an user control on the error branch where we don't leak exception (or more generally, any interrupts)

[3]: porcelain means implicit invariants held in the mind of the programmer (or the assertions/comments).

The new `decompress` API

The new decompress keeps the same inflation logic, but drastically changes the deflator to make the flush operation clearer. For many purposes, people don't want to hand-craft their compressed flows – they just want of_string/to_string functions. However, in some contexts (like a PNG encoder/decoder), the user should be able to play with decompress in detail (OpenPGP needs this too in RFC 4880).

The Zlib format

Both decompress and zlib use Huffman coding, an algorithm for building a dictionary of variable-length codewords for a given set of symbols (in this case, bytes). The most common byte is assigned the shortest bit sequence; less common bytes are assigned longer codewords. Using this dictionary, we just translate each byte into its codeword and we should achieve a good compression ratio. Of course, there are other details, such as the fact that all Huffman codes are prefix-free. The compression can be taken further with the LZ77 algorithm.

The zlib format, a superset of the RFC 1951 format, is easy to understand. We will only consider the RFC 1951 format, since zlib adds only minor details (such as checksums). It consists of several blocks: DEFLATE blocks, each with a little header, and the contents. There are 3 kinds of DEFLATE blocks:

a FLAT block; no compression, just a blit from inputs to the current block.
a FIXED block; compressed using a pre-computed Huffman code.
a DYNAMIC block; compressed using a user-specified Huffman code.

The FIXED block uses a Huffman dictionary that is computed when the OCaml runtime is initialised. DYNAMIC blocks use dictionaries specified by the user, and so these must be transmitted alongside the data (after being compressed with another Huffman code!). The inflator decompresses this DYNAMIC dictionary and uses it to do the reverse translation from bit sequences to bytes.

Inflator

The design of the inflator did not change a lot from the last version of decompress. Indeed, it's about to take an input, compute it and return an output like a flow. Of course, the error case can be reached.

So the API is pretty-easy:

val decode : decoder -> [ `Await | `Flush | `End | `Malformed of string ]

As you can see, we have 4 cases: one which expects more inputs (Await), the second which asks to the user to flush internal buffer (Flush), the End case when we reach the end of the flow and the Malformed case when we encounter an error.

For each case, the user can do several operations. Of course, about the Await case, they can refill the contents with an other inputs buffer with:

val src : decoder -> bigstring -> off:int -> len:int -> unit

This function provides the decoder a new input with len bytes to read starting at off in the given bigstring.

In the Flush case, the user wants some information like how many bytes are available in the current output buffer. Then, we should provide an action to flush this output buffer. In the end, this output buffer should be given by the user (how many bytes they want to allocate to store outputs flow).

type src = [ `Channel of in_channel | `Manual | `String of string ]

val dst_rem : decoder -> int
val flush : decoder -> unit
val decoder : src -> o:bigstring -> w:bigstring -> decoder

The last function, decoder, is the most interesting. It lets the user, at the beginning, choose the context in which they want to inflate inputs. So they choose:

src, where come from inputs flow
o, output buffer
w, window buffer

o will be used to store inflated outputs, dst_rem will give to us how many bytes inflator stored in o and flush will just set decoder to be able to recompute the flow.

w is needed for lz77 compression. However, as we said, we let the user give us this intermediate buffer. The idea behind that is to let the user prepare an inflation. For example, in ocaml-git, instead of allocating w systematically when we want to decompress a Git object, we allocate w one time per threads and all are able to use it and re-use it. In this way, we avoid systematic allocations (and allocate only once time) which can have a serious impact about performances.

The design is pretty close to one idea, a description step by the decoder function and a real computation loop with the decode function. The idea is to prepare the inflation with some information (like w and o) before the main (and the most expensive) computation. Internally we do that too (but it's mostly about a macro-optimization).

It's the purpose of OCaml in general, be able to have a powerful way to describe something (with constraints). In our case, we are very limited to what we need to describe. But, in others libraries like angstrom, the description step is huge (describe the parser according to the BNF) and then, we use it to the main computation, in the case of angstrom, the parsing (another example is [cmdliner][cmdliner]).

This is why decoder can be considered as the main function where decode can be wrapped under a stream.

Deflator

The deflator is a new (complex) deal. Indeed, behind it we have two concepts:

the encoder (according to RFC 1951)
the compressor

For this new version of decompress, we decide to separate these concepts where one question leads all: how to put my compression algorithm? (instead to use LZ77).

In fact, if you are interested in compression, several algorithms exist and, in some context, it's preferable to use lzwa for example or rabin's fingerprint (with duff), etc.

Functor

The first idea was to provide a functor which expects an implementation of the compression algorithm. However, the indirection of a functor comes with (big) performance cost. Consider the following functor example:

module type S = sig
  type t
  val add : t -> t -> t
  val one : t
end

module Make (S : S) = struct let succ x = S.add x S.one end

include Make (struct
  type t = int
  let add a b = a + b
  let one = 1
end)

let f x = succ x

Currently, with OCaml 4.07.1, the f function will be a caml_apply2. We might wish for a simple _inlining_ optimisation, allowing f to become an addq instruction (indeed, `flambda` does this), but optimizing functors is hard. As we learned from Pierre Chambart, it is possible for the OCaml compiler to optimize functors directly, but this requires respecting several constraints that are difficult to respect in practice.

Split encoder and compressor

So, the choice was done to made the encoder which respects RFC 1951 and the compressor under some constraints. However, this is not what zlib did and, by this way, we decided to provide a new design/API which did not follow, in first instance, zlib (or some others implementations like miniz).

To be fair, the choice from zlib and miniz comes from the first point about API and the context where they are used. The main problem is the shared queue between the encoder and the compressor. In C code, it can be hard for the user to deal with it (where they are liable for buffer overflows).

In OCaml and for decompress, the shared queue can be well-abstracted and API can ensure assumptions (like bounds checking).

Even if this design is much more complex than before, coverage tests are better where we can separately test the encoder and the compressor. It breaks down the initial black-box where compression was intrinsec with encoding – which was error-prone. Indeed, decompress had a bug about generation of Huffman codes but we never reached it because the (bad) compressor was not able to produce something (a specific lengh with a specific distance) to get it.

NOTE: you have just read the main reason for the new version of decompress!

The compressor

The compressor is the most easy part. The goal is to produce from an inputs flow, an outputs flow which is an other (more compacted) representation. This representation consists to:

A literal, the byte as is
A copy code with an offset and a length

The last one say to copy length byte(s) from offset. For example, aaaa can be compressed as [ Literal 'a'; Copy (offset:1, len:3) ]. By this way, instead to have 4 bytes, we have only 2 elements which will be compressed then by an Huffman coding. This is the main idea of the lz77 compression.

However, the compressor should need to deal with the encoder. An easy interface, à la uutf should be:

val compress : state -> [ `Literal of char | `Copy of (int * int) | `End | `Await ]

But as I said, we need to feed a queue instead.

At this point, the purpose of the queue is not clear and not really explained. The signature above still is a valid and understandable design. Then, we can imagine passing Literal and Copy directly to the encoder. However, we should (for performance purpose) use a delaying tactic between the compressor and the deflator[^4].

Behind this idea, it's to be able to implement an hot-loop on the encoder which will iter inside the shared queue and transmit/encode contents directly to the outputs buffer.

So, when we make a new state, we let the user supply their queue:

val state : src -> w:bistring -> q:queue -> state
val compress : state -> [ `Flush | `Await | `End ]

The Flush case appears when the queue is full. Then, we refind the w window buffer which is needed to produce the Copy code. A copy code is limited according RFC 1951 where offset can not be upper than the length of the window (commonly 32ko). length is limited too to 258 (an arbitrary choice).

Of course, about the Await case, the compressor comes with a src function as the inflator. Then, we added some accessors, literals and distances. The compressor does not build the Huffman coding which needs frequencies, so we need firstly to keep counters about that inside the state and a way to get them (and pass them to the encoder).

[4]: About that, you should be interesting by the reason of why GNU yes is so fast where the secret is just about buffering.

The encoder

Finally, we can talk about the encoder which will take the shared queue filled by the compressor and provide an RFC 1951 compliant output flow.

However, we need to consider a special detail. When we want to make a DYNAMIC block from frequencies and then encode the inputs flow, we can reach a case where the shared queue contains an opcode (a literal or a copy) which does not appear in our dictionary.

In fact, if we want to encode [ Literal 'a'; Literal 'b' ], we will not try to make a dictionary which will contains the 256 possibilities of a byte but we will only make a dictionary from frequencies which contains only 'a' and 'b'. By this way, we can reach a case where the queue contains an opcode (like Literal 'c') which can not be encoded by the pre-determined Huffman coding – remember, the DYNAMIC block starts with the dictionary.

Another point is about inputs. The encoder expects, of course, contents from the shared queue but it wants from the user the way to encode contents: which block we want to emit. So it has two entries:

the shared queue
an user-entry

So for many real tests, we decided to provide this kind of API:

type dst = [ `Channel of out_channel | `Buffer of Buffer.t | `Manual ]

val encoder : dst -> q:queue -> encoder
val encode : encoder -> [ `Block of block | `Flush | `Await ] -> [ `Ok | `Partial | `Block ]
val dst : encoder -> bigstring -> off:int -> len:int -> unit

As expected, we take the shared queue to make a new encoder. Then, we let the user to specify which kind of block they want to encode by the Block operation.

The Flush operation tries to encode all elements present inside the shared queue according to the current block and feed the outputs buffer. From it, the encoder can returns some values:

Ok and the encoder encoded all opcode from the shared queue
Partial, the outputs buffer is not enough to encode all opcode, the user should flush it and give to us a new empty buffer with dst. Then, they must continue with the Await operation.
Block, the encoder reachs an opcode which can not be encoded with the current block (the current dictionary). Then, the user must continue with a new Block operation.

The hard part is about the ping-pong game between the user and the encoder where a Block expects a Block response from the user and a Partial expects an Await response. But this design reveals something higher about zlib this time: the flush mode.

The flush mode

Firstly, we talk about mode because zlib does not allow the user to decide what they want to do when we reach a Block or a Ok case. So, it defines some under-specified _modes_ to apply a policy of what to do in this case.

In decompress, we followed the same design and see that it may be not a good idea where the logic is not very clear and the user wants may be an another behavior. It was like a black-box with a black-magic.

Because we decided to split encoder and compressor, the idea of the flush mode does not exists anymore where the user explicitly needs to give to the encoder what they want (make a new block? which block? keep frequencies?). So we broke the black-box. But, as we said, it was possible mostly because we can abstract safely the shared queue between the compressor and the encoder.

OCaml is an expressive language and we can really talk about a queue where, in C, it will be just an other array. As we said, the deal is about performance, but now, we allow the user the possibility to write their code in this corner-case which is when they reachs Block. Behaviors depends only on them.

APIs in general

The biggest challenge of building a library is defining the API - you must strike a compromise between allowing the user the flexibility to express their use-case and constraining the user to avoid API misuse. If at all possible, provide an intuitive API: force the user not to need to think about security issues, memory consumption or performance.

Avoid making your API so expressive that it becomes unusable, but beware that this sets hard limits on your users: the current decompress API can be used to build of_string / to_string functions, but the opposite is not true - you definitely cannot build a stream API from of_string / to_string.

The best advice when designing a library is to keep in mind what you really want and let the other details fall into place gradually. It is very important to work in an iterative loop of repeatedly trying to use your library; only this can highlight bad design, corner-cases and details.

Finally, use and re-use it on your tests (important!) and inside higher-level projects to give you interesting questions about your design. The last version of decompress was not used in ocaml-git mostly because the flush mode was unclear.

Hide

Derivations as computations (ICFP 2019 slides) — Andrej Bauer, Aug 21, 2019

I gave a keynote talk "Derivations as Computations" at ICFP 2019.

Slides with speaker notes: derivations-as-computations-icfp-2019.pdf
Demo file: demo-icfp2019.m31

Slides with speaker notes: derivations-as-computations-icfp-2019.pdf
Demo file: demo-icfp2019.m31

Abstract: According to the propositions-as-types reading, programs correspond to proofs, i.e., a term t of type A encodes a derivation D whose conclusion is t : A. But to be quite precise, D may have parts which are not represented in t, such as subderivations of judgmental equalities. In general, a term does not record an entire derivation, but only its proof relevant part. This is not a problem, as long as the missing subderivations can be reconstructed algorithmically. For instance, an equation may be re-checked, as long as we work in a type theory with decidable equality checking.

But what happens when a type theory misbehaves? For instance, the extensional type theory elides arbitrarily complex term through applications of the equality reflection principle. One may take the stance that good computational properties are paramount, and dismiss any type theory that lacks them – or one may look into the matter with an open mind.

If there is more to a derivation than its conclusion, then we should not equate the two. Instead, we can adopt a fresh perspective in which the conclusion is the result of a derivation. That is, we think of a derivation as a computation tree showing how to compute its conclusion. Moreover, the computation encoded by the derivation is effectful: proof irrelevance is the computational effect of discarding data, while checking a side condition is the effect of consulting an oracle. Where there are two computational effects, surely many others can be found.

Indeed, we may set up type theory so that any terminating computation represents a derivation, as long as the computational steps that construct type-theoretic judgments are guaranteed to be validated by corresponding inference rules. Common techniques found in proof assistants (implicit arguments, coercions, equality checking, etc.) become computational effects. If we allow the user to control the effects, say through the mechanism of Plotkin and Pretnar’s handlers for algebraic effects, we obtain a very flexible proof assistant capable of dealing with a variety type theories.

Hide

Deriving Slowly — Rudi Grinberg, Aug 20, 2019

There’s been some recent grumbling about the usability of ppx in OCaml, and instead of just letting it slide again, I’ve decided to do something constructive about this and write a little tutorial on how to write a deriving plugin.

Using OCaml to drive a Raspberry Pi robot car — Jane Street, Aug 19, 2019

Back when the Raspberry Pi was first released in 2012 Michael Bacarella wrote a blog post on using OCaml and Async on this little device. Since then installing OCaml via opam has become a pretty smooth experience and everything works out of the box when using Raspbian – the default Raspberry Pi distribution.

Do applied programming languages research at Jane Street! — Jane Street, Aug 16, 2019

As our Tools & Compilers team has grown, the kinds of projects we work on has become more ambitious. Here are some of the major things we’re currently working on:

X509 0.7 — Hannes Mehnert (hannes), Aug 15, 2019

Cryptographic material

Cryptographic material

Once a private and public key pair is generated (doesn't matter whether it is plain RSA, DSA, ECC on any curve), this is fine from a scientific point of view, and can already be used for authenticating and encrypting. From a practical point of view, the public parts need to be exchanged and verified (usually a fingerprint or hash thereof). This leads to the struggle how to encode this cryptographic material, and how to embed an identity (or multiple), capabilities, and other information into it. X.509 is a standard to solve this encoding and embedding, and provides more functionality, such as establishing chains of trust and revocation of invalidated or compromised material. X.509 uses certificates, which contain the public key, and additional information (in a extensible key-value store), and are signed by an issuer, either the private key corresponding to the public key - a so-called self-signed certificate - or by a different private key, an authority one step up the chain. A rather long, but very good introduction to certificates by Mike Malone is available here.

OCaml ecosystem evolving

More than 5 years ago David Kaloper and I released the initial ocaml-x509 package as part of our TLS stack, which contained code for decoding and encoding certificates, and path validation of a certificate chain (as described in RFC 5280). The validation logic and the decoder/encoder, based on the ASN.1 grammar specified in the RFC, implemented using David's asn1-combinators library changed much over time.

The OCaml ecosystem evolved over the years, which lead to some changes:

Camlp4 deprecation - we used camlp4 for stream parsers of PEM-encoded certificates, and sexplib.syntax to derive s-expression decoders and encoders;
Avoiding brittle ppx converters - which we used for s-expression decoders and encoders of certificates after camlp4 was deprecated;
Build and release system iterations - initially oasis and a packed library, then topkg and ocamlbuild, now dune;
Introduction of the result type in the standard library - we used to use [ `Ok of certificate option | `Fail of failure ];
No more leaking exceptions in the public API;
Usage of pretty-printers, esp with the fmt library val pp : Format.formatter -> 'a -> unit, instead of val to_string : t -> string functions;
Release of ptime, a platform-independent POSIX time support;
Release of rresult, which includes combinators for computation results;
Release of gmap, a Map whose value types depend on the key, used for X.509 extensions, GeneralName, DistinguishedName, etc.;
Release of domain-name, a library for domain name operations (as specified in RFC 1035) - used for name validation;
Usage of the alcotest unit testing framework (instead of oUnit).

More use cases for X.509

Initially, we designed and used ocaml-x509 for providing TLS server endpoints and validation in TLS clients - mostly on the public web, where each operating system ships a set of ~100 trust anchors to validate any web server certificate against. But once you have a X.509 implementation, every authentication problem can be solved by applying it.

Authentication with path building

It turns out that the trust anchor sets are not equal across operating systems and versions, thus some web servers serve sets, instead of chains, of certificates - as described in RFC 4158, where the client implementation needs to build valid paths and accept a connection if any path can be validated. The path building was initially in 0.5.2 slightly wrong, but fixed quickly in 0.5.3.

Fingerprint authentication

The chain of trust validation is useful for the open web, where you as software developer don't know to which remote endpoint your software will ever connect to - as long as the remote has a certificate signed (via intermediates) by any of the trust anchors. In the early days, before let's encrypt was launched and embedded as trust anchors (or cross-signed by already deployed trust anchors), operators needed to pay for a certificate - a business model where some CAs did not bother to check the authenticity of a certificate signing request, and thus random people owning valid certificates for microsoft.com or google.com.

Instead of using the set of trust anchors, the fingerprint of the server certificate, or preferably the fingerprint of the public key of the certificate, can be used for authentication, as optionally done since some years in jackline, an XMPP client. Support for this certificate / public key pinning was added in x509 0.2.1 / 0.5.0.

Certificate signing requests

Until x509 0.4.0 there was no support for generating certificate signing requests (CSR), as defined in PKCS 10, which are self-signed blobs containing a public key, an identity, and possibly extensions. Such as CSR is sent to the certificate authority, and after validation of ownership of the identity and paying a fee, the certificate is issued. Let's encrypt specified the ACME protocol which automates the proof of ownership: they provide a HTTP API for requesting a challenge, providing the response (the proof of ownership) via HTTP or DNS, and then allow the submission of a CSR and downloading the signed certificate. The ocaml-x509 library provides operations for creating such a CSR, and also for signing a CSR to generate a certificate.

Mindy developed the command-line utility certify which uses these operations from the ocaml-x509 library and acts as a swiss-army knife purely in OCaml for these required operations.

Maker developed a let's encrypt library which implements the above mentioned ACME protocol for provisioning CSR to certificates, also using our ocaml-x509 library.

To complete the required certificate authority functionality, in x509 0.6.0 certificate revocation lists, both validation and signing, was implemented.

Deploying unikernels

As described in another post, I developed albatross, an orchestration system for MirageOS unikernels. This uses ASN.1 for internal socket communication and allows remote management via a TLS connection which is mutually authenticated with a X.509 client certificate. To encrypt the X.509 client certificate, first a TLS handshake where the server authenticates itself to the client is established, and over that connection another TLS handshake is established where the client certificate is requested. Note that this mechanism can be dropped with TLS 1.3, since there the certificates are transmitted over an already encrypted channel.

The client certificate already contains the command to execute remotely - as a custom extension, being it "show me the console output", or "destroy the unikernel with name = YYY", or "deploy the included unikernel image". The advantage is that the commands are already authenticated, and there is no need for developing an ad-hoc protocol on top of the TLS session. The resource limits, assigned by the authority, are also part of the certificate chain - i.e. the number of unikernels, access to network bridges, available accumulated memory, accumulated size for block devices, are constrained by the certificate chain presented to the server, and currently running unikernels. The names of the chain are used for access control - if Alice and Bob have intermediate certificates from the same CA, neither Alice may manage Bob's unikernels, nor Bob may manage Alice's unikernels. I'm using albatross since 2.5 years in production on two physical machines with ~20 unikernels total (multiple users, multiple administrative domains), and it works stable and is much nicer to deal with than scp and custom hacked shell scripts.

Why 0.7?

There are still some missing pieces in our ocaml-x509 implementation, namely modern ECC certificates (depending on elliptic curve primitives not yet available in OCaml), RSA-PSS signing (should be straightforward), PKCS 12 (there is a pull request, but this should wait until asn1-combinators supports the ANY defined BY construct to cleanup the code), ... Once these features are supported, the library should likely be named PKCS since it supports more than X.509, and released as 1.0.

The 0.7 release series moved a lot of modules and function names around, thus it is a major breaking release. By using a map instead of lists for extensions, GeneralName, ..., the API was further revised - invariants that each extension key (an ASN.1 object identifier) may occur at most once are now enforced. By not leaking exceptions through the public interface, the API is easier to use safely - see let's encrypt, openvpn, certify, tls, capnp, albatross.

I intended in 0.7.0 to have much more precise types, esp. for the SubjectAlternativeName (SAN) extension that uses a GeneralName, but it turns out the GeneralName is as well used for NameConstraints (NC) in a different way -- IP in SAN is an IPv4 or IPv6 address, in CN it is the IP/netmask; DNS is a domain name in SAN, in CN it is a name starting with a leading dot (i.e. ".example.com"), which is not a valid domain name. In 0.7.1, based on a bug report, I had to revert these variants and use less precise types.

Conclusion

The work on X.509 was sponsored by OCaml Labs. You can support our work at robur by a donation, which we will use to work on our OCaml and MirageOS projects. You can also reach out to us to realize commercial products.

I'm interested in feedback, either via ~~twitter~~ hannesm@mastodon.social or an issue on the data repository.

Hide

BAP Knowledge Representation - Part 1 — The BAP Blog, Aug 15, 2019

An important part of BAP 2.0 is the new knowledge representation system, which drives all the new code. Given how important it is for understanding and using modern BAP, I decided to introduce it informally in a series of blog posts. This series is by no means a substitution for documentation or a tutorial, which will (I hope) follow. The intention is to describe the system in a friendly manner like I would describe it to my colleague in front of a whiteboard.

All information in BAP 2.0 is stor…

All information in BAP 2.0 is stored in the knowledge base, which is roughly a global storage of information which could be used by different components for information exchange. It is like a set of global variables but without common problems associated with the global mutable state since the knowledge system will prevent data anomalies by ensuring that all updates are consistent and firing up a fixed point computation in case of mutual dependencies between different variables.

This knowledge base is essentially a set of objects. Objects belong to classes. Classes denote what properties objects have. Classes are further subdivided into sorts, which we will discuss in a separate blog post.

Object properties could be read or written. It is also possible to associate triggers with a property. Triggers are called promises in our parlance. A promise is a function that will be called when a property of an object is accessed. The promises are stored procedures in our knowledge base and they act like the injection points for different plugins, e.g., a lifter is just a promise to provide the semantics property of an object of class core-theory:program. The promise itself can access any other properties of any other objects (which it can reach, of course), even including the property that it is providing (recursive case). Moreover, with each property, we can associate several promises (triggers). For example, we can have several lifters working at the same time. The knowledge system will take care of running and scheduling different promises and will compute the fixed point solution in linear time using stochastic fixed-point computation, and yadda, yadda. The point is that it will make it automatically and transparent to the user, and will guarantee the consistency of the result (e.g., that it doesn’t depend on the order of evaluation of promises). It is also important to understand, that once a triggered property is computed it will be stored and never recomputed again¹.

Now let’s look underneath the hood of the knowledge base to see what objects and classes do we have right now. If you will run bap ./exe -dknowledge you will find out that most of the objects that are currently stored in the base belong to the core-theory:program class. Later, we will add more classes, but to implement the Bap.Std interface this one was enough. So let’s take a particular object as an example. The knowledge base is printed in the following format: (<object> (<properties>)). If an object has a symbolic identifier associated with it, then it will be printed, otherwise, a numeric identifier (basically a pointer) will be printed. The object class is not printed, but all objects are grouped by their class, with each new class opened with the (in-class <class-name>) statement. Also, note that all symbolic identifiers are properly namespaced, using the package system which is the same as in Common Lisp. All identifiers which do not belong to the current package, denoted with the (in-package <pkg>) statement, are printed as <package>:<name>).

Now, we are ready to read the output of -dknowledge. In the following output, we have an object, that belongs to the core-theory:program class, which has a printed representation core-theory:0x402fd0. The printed representation looks very much like a number, and you may notice that it is indeed equal to the address of an instruction which this object denotes.

(in-class core-theory:program)
<snip>
(core-theory:0x402fd0
  ((core-theory:label-addr (0x402fd0))
   (bap.std:arch (x86_64))
   (bap.std:insn ((MOV32rr EAX ESI)))
   (bap.std:mem ((402fd0 2 LittleEndian)))
   (core-theory:semantics
      ((bap.std:ir-graph
         ("00004b45:
           00004b46: RAX := pad:64[low:32[RSI]]"))
       (bap.std:insn-dests ((77054)))
       (bap.std:insn-ops ((EAX ESI)))
       (bap.std:insn-asm "movl %esi, %eax")
       (bap.std:insn-properties
          ((:invalid false) (:jump false) (:cond false)
           (:indirect false)
           (:call false) (:return false) (:barrier false)
           (:affect-control-flow false)
           (:load false) (:store false)))
       (bap.std:bil "{RAX := pad:64[low:32[RSI]]}")
       (bap.std:insn-opcode MOV32rr)))))

We can see, that the object is having the following properties:

core-theory:semantics - the semantics of this instruction
core-theory:label-addr - the address
bap.std:insn – the disassembled instruction
bap.std:mem - the region of memory which this instruction occupies
bap.std:arch - and the architecture

We can immediately infer a novel feature of bap 2.0, is that architecture is now a property of a particular instruction object (basically of an address), not of the whole project. Which enables multi-architectural analysis, where in the same base we have programs from different architectures, calling each other (ARM/Thumb is a good example).

The label-addr, insn, and mem properties are pretty self-explanatory, so let’s jump to the most interesting property called semantics. The semantics itself is also a set of properties, which is called a value. Later, we will discover that essentially objects are pointers to values. A value, like an object, also belongs to some class and has some properties. The core-theory:semantics property belongs to the core-theory:effect class. This class denotes general effects that are produced when an instruction is executed. In other words, the semantics of an instruction. The semantics may have many different denotations, i.e., we can use different mathematical objects and structures to represent the semantics, which we will discuss in details the later blog posts. But for now let’s briefly look into different denotations of semantics (which all belong to the bap.std package, so we will omit the package name for brevity):

bil - good old BAP 1.x BIL
ir-graph - the semigraphical BIR representation
insn-dests - the set of destinations
insn-opcode - the opcode
insn-ops - an array of operands
insn-asm - the assembly string
insn-properties - semantic properties provided by the decoder

As we may see, most of those properties are good old properties of the Bap.Std.Insn data type in BAP 1.x, and indeed in BAP 2.x Bap.Std.Insn.t is represented as a Knowledge.value instance. The only new field is the set of destinations, which denote a set of program objects that are reachable from the given address. Which lets us explore the whole graph.

This brings us to the end of the first blog post about BAP 2.0 and the new knowledge system. We will discuss the knowledge system, along with an actual program interface in the upcoming blog posts. To make those posts productive I encourage everyone to join the discussion of BAP 2.0 in our gitter channel. Please, feel free to provide feedback, ask questions and drive the future posts.

¹⁾ All this magic with the consistent state, fixed-point solutions, etc is possible due to one trick - a data type of any property in our knowledge base must form a domain. A domain is a set equipped with a partial order and a special element called the bottom, so a domain is a generalization of a lattice (all lattices are domains, but not all domains are lattices). The partial order associated with the data type orders elements of this type by the amount of information. The knowledge system guarantees that all updates to object values preserve knowledge, i.e., the value of a property can never become less (wrt to the associated partial order), than it was before. Going deeper into details, every time a property is updated the existing value is joined with the new value, x = join old new, where the join operation is either induced by the domain order associated with the data type, or provided by a user (which basically allows users to register their lattices). To handle cases where join doesn’t exist (and it may not exist, since we’re not requiring lattices), we extend the user datum with the top value which denotes conflicting information (therefore named conflict), thus turning each domain into dcpo (directed complete partial order - the structure that we actually need, to ensure all those magical properties, dcpo is very close to a lattice, but still a little bit more general).

Hide

Down — Daniel Bünzli, Jul 23, 2019

First release of Down, an unintrusive OCaml toplevel experience upgrade.

View older blog posts.

OCaml Planet

On fixed-point theorems in synthetic computability — Andrej Bauer, Nov 06, 2019

Runners in action — Andrej Bauer, Oct 27, 2019

Coq 8.10.1 is out — Coq, Oct 25, 2019

Announcing MirageOS 3.6.0 — MirageOS (Martin Lucina), Oct 18, 2019

MirageOS 3.6.0 release

MirageOS 3.6.0 release

Commas in big numbers everywhere: An OpenType adventure — Jane Street, Oct 14, 2019

Coq 8.10.0 is out — Coq, Oct 07, 2019

OCaml expert and beginner training by OCamlPro (in French): Nov. 5-6 & 7-8 — OCamlPro, Sep 25, 2019

Mr. MIME - Parse and generate emails — Tarides (Romain Calascibetta), Sep 25, 2019

An email parser

An email parser

An extended email parser

A realistic email parser

A parser usable by others

An email generator

78-character rule

A multipart email generator

Behind the forest

Rosetta

Pecu and Base64

Conclusion

A look back on OCaml since 2011 — OCamlPro, Sep 20, 2019

2011

2012

2013

2014

2015

2016

2017

2018

2019

Frama-C 19.1 (Potassium) is out. Download ithere. — Frama-C, Sep 17, 2019

Coq 8.10+beta3 is out — Coq, Sep 16, 2019

OCaml Developer at Ahrefs Pte Ltd (Full-time) — Functional Jobs (FunctionalJobs.com), Sep 14, 2019

Compiler Engineer at Axoni (Full-time) — Functional Jobs (FunctionalJobs.com), Sep 13, 2019

Updated Cheat Sheets: OCaml Language and OCaml Standard Library — OCamlPro, Sep 13, 2019

Frama-Clang 0.0.7 is out. Download ithere. — Frama-C, Sep 13, 2019

Decompress: Experiences with OCaml optimization — Tarides (Romain Calascibetta), Sep 13, 2019

Cautionary advice

Specialization

Results

Inlining

In decompress

Untagged integers

Readability versus performance

Exceptions

Unrolling

Results

hot-loop

caml_modify

About decompress

Smaller representation

Conclusion

On complete ordered fields — Andrej Bauer, Sep 08, 2019

An introduction to fuzzing OCaml with AFL, Crowbar and Bun — Tarides (Nathan Rebours), Sep 04, 2019

What is AFL?

Using AFL to fuzz an OCaml parser

Using Crowbar and AFL for property-based testing

Using bun to run fuzz testing in CI

Final words

What is algebraic about algebraic effects? — Andrej Bauer, Sep 02, 2019

The blog moved from Wordpress to Jekyll — Andrej Bauer, Sep 02, 2019

OCamlPro’s compiler team work update — OCamlPro, Aug 30, 2019

Short-term improvements

Recursive values compilation

Separate compilation of recursive modules, compilation units as functors

Small improvements to Flambda

Flambda 2.0

What the interns have wrought, 2019 edition — Jane Street, Aug 30, 2019

Decompress: The New Decompress API — Tarides (Romain Calascibetta), Aug 26, 2019

API design

A dbuenzli API

The new decompress API

The Zlib format

Inflator

Deflator

Functor

Split encoder and compressor

In `decompress`

About `decompress`

Using `bun` to run fuzz testing in CI

The new `decompress` API