At Ahrefs, we have been using BuckleScript and ReasonML in production for more than two years. We already have a codebase of tens of thousands of lines of code, with several web applications that are data intensive and communicate with backend services written in OCaml, using tools like atd.

Given our investment in these technologies, we have been following closely the recent changes in ReScript, with its rebrand and renaming, and the split with the ReasonML proje…

At Ahrefs, we have been using BuckleScript and ReasonML in production for more than two years. We already have a codebase of tens of thousands of lines of code, with several web applications that are data intensive and communicate with backend services written in OCaml, using tools like atd.

Given our investment in these technologies, we have been following closely the recent changes in ReScript, with its rebrand and renaming, and the split with the ReasonML project, explained in the project blog post.

ReScript: becoming its own language

We are excited about the way ReScript is unifying the experience and making it easier for developers who are getting started to find documentation in a single place, as well as continuing its strong focus on performance and readable JavaScript output.

On the other hand, we are trying to figure out the implications of this change in the mid- and long-term, especially regarding the integration with the OCaml ecosystem. And more importantly, what this evolution will mean for production users like us who rely on this integration.

ReScript integration with OCaml has historically been seamless, as BuckleScript started originally as a new backend for the OCaml compiler. However, in recent months, there have been several hints that ReScript wants to evolve towards becoming its own language:

• It has now its own parser, incompatible with OCaml native applications
• Official repository guidelines for technical writing mentions explicitly that no reference to OCaml should appear in docs
• Upgrades to the latest version of OCaml compiler, which used to be part of the roadmap, have been deprioritized recently.

So, even if officially ReScript has not announced that they will break backwards compatibility with OCaml, just the fact that it is sticking with an old version of the OCaml compiler poses some challenges for us in terms of tooling. The uncertainty about the future and the pace of changes add some risk to the high-level goals we have for our teams and codebase: we would like to share more code between frontend and backend, not less.

Melange: a fork of ReScript, focused on OCaml compatibility

When António Monteiro announced Melange, a fork of ReScript but with a strong focus on keeping compatibility with OCaml, we decided to try it out and see how it could work for us.

Ultimately, the experiment was successful. We managed to build all our frontend applications with Melange, while keeping the existing bundling setup, which currently uses Webpack.

Throughout this process, we had to modify some parts of the code. We will now go through the most relevant parts of the process:

• Upgrade to OCaml 4.12: the most relevant part was the deprecation of Pervasives module to use Stdlib.
• Use ppxlib in our ppxs: we had to upgrade the two ppxs that we use in the frontend codebase to the latest compiler version, bs-emotion-ppx and an in-house ppx for internationalization.
• Configure esy: we were already using esy to bring the editor tooling into scope of the developer environment, so we just had to make sure melange would also be included in the json configuration.
• Upgrade to Reason 3.7.0: a quite simple change too, as the whole process is automated by using refmt. As a side note, we ran into a small bug with some type annotations, that we were able to work around.
• “Lift” dune workspace to the root of our monorepo: this is probably the most intrusive change. Because we have shared code between backend and frontend, and Dune needs to have access to all sources under its workspace, we had to “lift” the Dune workspace from the backend directory to the root of monorepo.

The good

This experiment allowed us to experience what a project like Melange could offer for our use case. Here are some of the things we might be able to leverage in a codebase built with Melange:

• Recent version of the OCaml compiler: at some point, we could pin compiler version between backend and frontend teams, making upgrades more straightforward as they would happen atomically.
• Shared editor tooling: the official OCaml vscode extension works great with Melange, as well as any other OCaml editor integration. Having backend and frontend teams use similar editor setup removes a lot of maintenance work for us.
• Consuming ppxs from source: Melange allows to consume ppxs from source, which also removes issues with pre-compiled ppxs (like this issue with the recent M1 Macs).
• Melange allows to run all ppxs from a single executable file, which has some nice performance benefits.
• Use Dune for atd files generators: ReScript “generators” are unfortunately not documented anymore, but we use them extensively for atd file generation. Being able to share Dune rules in backend and frontend would make our build setup easier.
• Access to OCaml documentation tooling: Melange allows to leverage existing tooling for generating documentation, like odoc.
• Async syntax: the latest Reason version supports “let op” syntax, which is handy for client-side code.

The bad

While there are many things that are exciting about Melange, there are some other parts that can be improved.

• Build performance: We already knew that performance would be far worse than ReScript, as Melange uses Dune in a way that it was not designed for. In our tests, builds with Melange are roughly 1 order of magnitude slower than ReScript ones.
• First-class Dune support: if there was a deeper integration between Dune and Melange, we could explore features like shared libraries or shared rules between backend and frontend. As of today, Dune has no knowledge about Melange environment, so it can perform basic rules execution, but there is no access to high level stanzas like library in Melange.
• Two-headed goal: finally, we see a more strategic risk in Melange proposition. Right now it has two goals: keep compatibility with both ReScript and OCaml. But we don’t know how long these goals will be feasible. If at some point ReScript decides to move away from the OCaml compiler fully, then Melange users would not be able to consume any updates to the ReScript ecosystem anymore.

Alright, but are you migrating to Melange or ReScript?

With all the information available, the answer is: we don’t know yet. 😄 We want to keep exploring all the available options and have as much information as possible before committing further. So for now, we are upgrading the codebase to recent versions of ReScript, but we are holding up on features that only work one way. For example, we have not migrated our codebase to the ReScript syntax yet, as there is no way to translate back to Reason syntax.

In the meantime, we will keep exploring how far the limitations of Melange can be mitigated. To be continued! 🚀

Thanks to Igor and Feihong for reviewing and improving earlier versions of this post.

Building Ahrefs codebase with Melange was originally published in ahrefs on Medium, where people are continuing the conversation by highlighting and responding to this story.

A while ago, my former student Chuangjie Xu and I computed an integer using a sheaf topos. For that purpose,

1. we developed our mathematics constructively,
2. we formalized our mathematics in Martin-Löf type theory, in Agda notation,
3. we pressed a button, and
4. after a few seconds we saw the integer we expected in front of us.

Well, it was a few seconds for the computer in steps (3)-(4), but three years for us in steps (1)-(2).

Why formalize?

Most people formalize mathematics (in Automa…

A while ago, my former student Chuangjie Xu and I computed an integer using a sheaf topos. For that purpose,

1. we developed our mathematics constructively,
2. we formalized our mathematics in Martin-Löf type theory, in Agda notation,
3. we pressed a button, and
4. after a few seconds we saw the integer we expected in front of us.

Well, it was a few seconds for the computer in steps (3)-(4), but three years for us in steps (1)-(2).

Why formalize?

Most people formalize mathematics (in Automath, NuPrl, Coq, Agda, Lean, ...) to get confidence in the correctness of mathematics - or so they claim. The reality is that formalizing mathematics is intellectually fun.

Entertaining considerations aside, my initial motivation for computer formalization, about 10 years ago, was to write algorithms derived from work on game theory with Paulo Oliva. In particular, this had applications to proof theory, such as getting programs from classical proofs. Our first version of a (manually) extracted program from a classical proof was written in Haskell, in a train journey coming back from a visit to our collaborators Monika Seisenberger and Ulrich Berger in Swansea. The train journey was long enough for us to be able to complete the program. But when we ran it, it didn't work. I had been learning Agda for about one year by then, and I told Paulo that it would be easier to write the mathematics in Agda, and hence be sure it will work before we ran it, than to debug the Haskell program. And that was the case.

Before then I was the kind of person who dismissed formalization, and would say so to people who did formalization (it is probably too late to apologize now). I trusted my own mathematics, and if I wanted to derive programs from my mathematical work, I would just write them manually. Since then, my attitude has changed considerably.

I now use Agda as a "blackboard" to develop my work. For example, the following were conceived and developed directly in Agda before they were written in mathematical vernacular: Injective types in univalent mathematics, Compact, totally separated and well-ordered types in univalent mathematics, The Cantor-Schröder-Bernstein Theorem for ∞-groupoids, The Burali-Forti argument in HoTT/UF and Continuity of Gödel's system T functionals via effectful forcing.

Other people will have different reasons to formalize. For example, wouldn't it be wonderful if the whole undergraduate mathematical curriculum were formalized? Wouldn't it be wonderful to archive all mathematical knowledge not just as text but in a more structured way, so that it can be used by both people and computers? Wouldn't it be wonderful if when we submit a paper, the referee didn't need to check correctness, but only novelty, significance and so on? Did you ever woke up in the middle of the night after you submitted a paper, with doubts about the crucial lemma? Or worse, after it was published?

But for the purposes of this post, I will concentrate on only one aspect of formalization: a formalized piece of constructive mathematics is automatically a computer program that you can run in practice.

Constructive mathematics

Constructive mathematics begins by removing the principle of excluded middle, and therefore the axiom of choice, because choice implies excluded middle. But why would anybody do such an outrageous thing?

I particularly like the analogy with Euclidean geometry. If we remove the parallel postulate, we get absolute geometry, also known as neutral geometry. If after we remove the parallel postulate, we add a suitable axiom, we get hyperbolic geometry, but if we instead add a different suitable axiom we get elliptic geometry. Every theorem of neutral geometry is a theorem of these three geometries, and more geometries. So a neutral proof is more general.

When I say that I am interested in constructive mathematics, most of the time I mean that I am interested in neutral mathematics, so that we simply remove excluded middle and choice, and we don't add anything to replace them. So my constructive definitions and theorems are also definitions and theorems of classical mathematics.

Occasionally, I flirt with axioms that contradict the principle of excluded middle, such as Brouwerian intuitionistic axioms that imply that "all functions $(\mathbb{N} \to 2) → \mathbb{N}$ are uniformly continuous", when we equip the set $2$ with the discrete topology and $\mathbb{N} \to 2$ with the product topology, so that we get the Cantor space. The contradiction with classical logic, of course, is that using excluded middle we can define non-continuous functions by cases. Brouwerian intuitionistic mathematics is analogous to hyperbolic or elliptic geometry in this respect. The "constructive" mathematics I am talking about in this post is like neutral geometry, and I would rather call it "neutral mathematics", but then nobody would know what I am talking about. That's not to say that the majority of mathematicians will know what I am talking about if I just say "constructive mathematics".

But it is not (only) the generality of neutral mathematics that I find attractive. Somehow magically, constructions and proofs that don't use excluded middle or choice are automatically programs. The only way to define non-computable things is to use excluded middle or choice. There is no other way. At least not in the underlying type theories of proof assistants such as NuPrl, Coq, Agda and Lean. We don't need to consider Turing machines to establish computability. What is a computable sheaf, anyway? I don't want to pause to consider this question in order to use a sheaf topos to compute a number. We only need to consider sheaves in the usual mathematical sense.

Sometimes people ask me whether I believe in the principle of excluded middle. That would be like asking me whether I believe in the parallel postulate. It is clearly true in Euclidean geometry, clearly false in elliptic and in hyperbolic geometries, and deliberately undecided in neutral geometry. Not only that, in the same way as the parallel postulate defines Euclidean geometry, the principle of excluded middle and the axiom of choice define classical mathematics.

The undecidedness of excluded middle in my neutral mathematics allows me to prove, for example, "if excluded middle holds, then the Cantor-Schröder-Bernstein Theorem for ∞-groupoids holds". If excluded middle were false, I would be proving a counter-factual - I would be proving that an implication is true simply because its premise is false. But this is not what I am doing. What I am really proving is that the CSB theorem holds for the objects of boolean ∞-toposes. And why did I use excluded middle? Because somebody else showed that there is no other way. But also sometimes I use excluded middle or choice when I don't know whether there is another way (in fact, I believe that more than half of my publications use classical logic).

So, am I a constructivist? There is only one mathematics, of which classical and constructive mathematics are particular branches. I enjoy exploring the whole landscape. I am particularly fond of constructive mathematics, and I wouldn't practice it, however useful it may be for applications, if I didn't enjoy it. But this is probably my bad taste.

Toposes as provinces of the mathematical world

Toposes are generalized (sober) spaces. But also toposes can be considered as provinces of the mathematical world.

Hyland's effective topos is a province where "everything is computable". This is an elementary topos, which is not a Grothendieck topos, built from classical ingredients: we use excluded middle and choice, with Turing machines to talk about computability. But, as it turns out, although everybody agrees which functions $\mathbb{N} \to \mathbb{N}$ are computable and which ones aren't, there is disagreement among classical mathematicians working on computability theory about what counts as "computable" for more general mathematical objects, such as functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$. No problem. Just consider other provinces, called realizability toposes, which include the effective topos as an example.

Johnstone's topological topos is a topos of spaces. It fully embeds a large category of topological spaces, where the objects outside the image of the embedding can be considered as generalized spaces (which include the Kuratowski limit spaces and more). In this province of the mathematical world, "all functions are continuous".

There are also provinces where there are infinitesimals and "all functions are smooth".

A more boring, but important, province, is the topos of classical sets. This is where classical mathematics takes place.

These provinces of mathematics have an internal language. We use a certain subobject classifier to collect the things that count as truth values in the province, and we devise a kind of type theory whose types are interpreted as objects and whose mathematical statements are interpreted as truth values in the province. Then a mathematical statement in this type theory is true in some toposes, false in other toposes, and undecided in yet other toposes. This internal language, or type theory, is very rich. Starting from natural numbers we can construct the integers, the rationals, the real numbers, free groups etc., and then do e.g. analysis and group theory and so on. The internal language of the free topos can be considered as a type theory for neutral mathematics: whatever we prove in the free type theory is true in all mathematical provinces, including classical set theory.

In the above first three provinces, the principle of excluded middle fails, but for different reasons, with respectively computability, continuity and infinitesimals to blame.

Our topos

Now our plot has a twist: we work within neutral mathematics to build a province of "biased" constructive mathematics where Brouwerian principles hold, such as "all functions $(\mathbb{N} \to 2) → \mathbb{N}$ are uniformly continuous".

Johnstone's topological topos (1979) would do the job, except that it is built using classical ingredients. This topos has siblings by Mike Fourman (1982) and van der Hoeven and Moerdijk (1984) with aims similar to ours, as explained in our own 2013 and 2016 papers, which give a third sibling.

Johnstone's topological topos is very easy to describe: take the monoid of continuous endomaps of the one-point compactification of the discrete natural numbers, considered as a category, then take sheaves for the canonical coverage. Van der Hoeven and Moerdijk's topos is similar: this time take the monoid of continuous endomaps of the Baire space, with the "open-cover coverage". Fourman's topos is constructed from a site of formal spaces or locales, with a similar coverage.

Our topos is also similar: we take the monoid of uniformly continuous endomaps of the Cantor space. Because it is not provable in neutral mathematics that continuous functions on the Cantor space are automatically uniformly continuous, we explicitly ask for uniform continuity rather than just continuity. As for our coverage, we initially considered coverings of finitely many jointly surjective maps. But an equivalent, smaller coverage makes the mathematics (and the formalization) simpler: for each natural number $n$ we consider a cover with $2^n$ functions, namely the concatenation maps $(\mathbb{N} \to 2) \to (\mathbb{N} \to 2)$ defined by $\alpha \mapsto s \alpha$ for each finite binary sequence $s$ of length $n$. These functions are jointly surjective, and, moreover, have disjoint images, considerably simplifying the checking of the sheaf condition. Moreover, the coverage axiom is not only satisfied, but also is equivalent to the fact that the morphisms in our site are uniformly continuous functions. So this is a sort of "uniform-continuity coverage". Our slides (2014) illustrate these ideas with pictures and examples.

The details of the mathematics can be found in the above paper, and the Agda formalization can be found at Chuangjie's page. A few years later, we ported part of this formalization to Cubical Agda to deal properly with function extensionality (which we originally dealt with in ad hoc ways).

The integer we compute

After we construct the sheaf topos, we define a simple type theory and we interpret it in the topos. We define a "function" $(\mathbb{N} \to 2) \to \mathbb{N}$ in this type theory, without proving that it is uniformly continuous, and apply the interpretation map to get a morphism of the topos, which amounts to a uniformly continuous function. From this morphism we get the modulus of uniform continuity, which is the integer we are interested in. The interested reader can find the details in the above paper and Agda code for the paper or the substantially more comprehensive Agda code for Chuangjie's thesis.

Tarides is taking part in the Data Portability & Services Incubator (DAPSI), a 3-year EU funded project that empowers internet innovators to develop new solutions in the Data Portability field.

What is DAPSI?

The Data Portability and Services Incubator (DAPSI) is an EU funded project, under the European Commission’s Next Generation Internet (NGI) initiative. The aim of this initiave is to empower top internet innovators to develop human-centric solutions. DAPSI addresses the challenge of …

Tarides is taking part in the Data Portability & Services Incubator (DAPSI), a 3-year EU funded project that empowers internet innovators to develop new solutions in the Data Portability field.

What is DAPSI?

The Data Portability and Services Incubator (DAPSI) is an EU funded project, under the European Commission’s Next Generation Internet (NGI) initiative. The aim of this initiave is to empower top internet innovators to develop human-centric solutions. DAPSI addresses the challenge of personal data portability on the internet, as foreseen under the GDPR and make it significantly easier for citizens to have any data which is stored with one service provider transmitted directly to another provider.

Take a look at the DAPSI innovators portfolio to see more information about the selected projects.

What is our project?

Our project, called SCoP for Secure-by-design Communication Protocols, is taking part in the DAPSI to tackle data portability issues in communication services.

Over the past few decades, the usage of emails has been massively widespread by both individuals and companies. Billions of emails are sent every day and this number is expected to increase to reach 333 billion of emails exchanged daily in 2022. Moreover, as managing internet communication stacks have become increasingly complex, end-users have tended to entrust this task to third-party companies like Google and Microsoft. Furthermore, existing implementations of these communication services rely on ad-hoc methodologies and memory-unsafe languages, where minor developer errors can easily escalate into major security flaws. The centralization of these communication services means that a single successful attack leads to major personal data breaches.

To fix this issue, our project aims to engineer a modern basis for open messaging that supports existing protocols such as emails but is also extensible and customizable for emerging protocols such as matrix. We will be building trustable implementations of these open protocols using type-safe languages and we will deploy these implementations as specialized, secure and resource efficient unikernels. They will become the basis of the communication system of OSMOSE, Tarides’ commercial solution for secure-by-design IoT infrastructure.

Every component of that system will be carefully designed as independent libraries, using modern development techniques to avoid the common reported threats and flaws. For instance, the implementation of protocol parsers and serializers will be written in a type-safe language and will be using fuzzing, e.g state-of-the-art coverage-driven tests. The combination of these techniques will increase users’ trust to migrate their personal data to these new secure services.

Moreover, these techniques are also useful to produce a large and reusable corpus of test materials, which we plan to release separately for other implementations to use. It will give the tools to other developers to write the next generation of messaging applications by extending the existing protocols with more confidence.

Want to be part of it?

Would you like to hear more about the project? Or want to deploy our solution? This project will build on a number of existing components in MirageOS, such as MrMime and Irmin, so feel free to contribute to these existing components! Please reach out to contact@tarides.com.

The third annual meeting of the Alt-Ergo Users’ Club took place on April 1! Our annual meeting is the ideal place to review the needs of each partner regarding Alt-Ergo. We were pleased to welcome our partners to discuss the roadmap for future Alt-Ergo developments and improvements.

Alt-Ergo is an automatic prover of mathematical formulas, jointly developed by LRI and OCamlPro (since 2014). To learn more or join the Club, visit https://alt-ergo.ocamlpro.com.

Our Club has several goa…

The third annual meeting of the Alt-Ergo Users’ Club took place on April 1! Our annual meeting is the ideal place to review the needs of each partner regarding Alt-Ergo. We were pleased to welcome our partners to discuss the roadmap for future Alt-Ergo developments and improvements.

Alt-Ergo is an automatic prover of mathematical formulas, jointly developed by LRI and OCamlPro (since 2014). To learn more or join the Club, visit https://alt-ergo.ocamlpro.com.

Our Club has several goals. Its main objective is to ensure the sustainability of Alt-Ergo by fostering collaboration between Club members and by building links with users of formal methods, such as the Why3 community. One of our priorities is to define the needs of users of constraint solvers by extending Alt-Ergo to new domains such as Model Checking, while competing with other state-of-the-art solvers in international competitions. Finally, the Club aims to find new projects or contracts for the development of long term functionalities.

We would like to thank all our members for their support: Mitsubishi Electric R&D Centre Europe, AdaCore and CEA List. We would also like to acknowledge the help of the Why3 development team with whom we work to improve our tools.

This year, new points of interest were raised by our members. Firstly, model generation, which was added to Alt-Ergo in the last edition, has been useful to the majority of our club members. Firstly, we will now focus on refining the constraints and studying how to propagate them. Secondly, we presented Dolmen: the parser/typer that will allow to type only once SMT2 files and to be ready for SMT3. Its integration to Alt-Ergo is in progress. The opinion of the club members is warm about the future contributions of the Dolmen tool to the SMT solver community!

These features are now our main priorities. You can see the boards presented at the 2021 Club meeting. To follow our progress on the new features, follow the articles on our blog!

About OCamlPro:

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users’ Club). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: contact@ocamlpro.com.

Introduction

Tl;DR: mirage-crypto-ec, with x509 0.12.0, and tls 0.13.0, provide fast and secure elliptic curve support in OCaml and MirageOS - using the verified fiat stack (Coq to OCaml to executable which generates C code that is interfaced by OCaml). In x509, a long standing issue (countryName encoding), and archive (PKCS 12) format is now supported, in addition to EC keys. In tls, ECDH key exchanges are supported, and ECDSA and EdDSA certificates.

Elliptic curve cryptography

Since May 2020, …

Introduction

Tl;DR: mirage-crypto-ec, with x509 0.12.0, and tls 0.13.0, provide fast and secure elliptic curve support in OCaml and MirageOS - using the verified fiat stack (Coq to OCaml to executable which generates C code that is interfaced by OCaml). In x509, a long standing issue (countryName encoding), and archive (PKCS 12) format is now supported, in addition to EC keys. In tls, ECDH key exchanges are supported, and ECDSA and EdDSA certificates.

Elliptic curve cryptography

Since May 2020, our OCaml-TLS stack supports TLS 1.3 (since tls version 0.12.0 on opam).

TLS 1.3 requires elliptic curve cryptography - which was not available in mirage-crypto (the maintained fork of nocrypto).

There are two major uses of elliptic curves: key exchange (ECDH) for establishing a shared secret over an insecure channel, and digital signature (ECDSA) for authentication, integrity, and non-repudiation. (Please note that the construction of digital signatures on Edwards curves (Curve25519, Ed448) is called EdDSA instead of ECDSA.)

Elliptic curve cryptoraphy is vulnerable to various timing attacks - have a read of the overview article on ECDSA. When implementing elliptic curve cryptography, it is best to avoid these known attacks. Gladly, there are some projects which address these issues by construction.

In addition, to use the code in MirageOS, it should be boring C code: no heap allocations, only using a very small amount of C library functions -- the code needs to be compiled in an environment with nolibc.

Two projects started in semantics, to solve the issue from the grounds up: fiat and hacl-star: their approach is to use a proof system (Coq or F* to verify that the code executes in constant time, not depending on data input. Both projects provide as output of their proof systems C code.

For our initial TLS 1.3 stack, Clément, Nathan and Etienne developed fiat-p256 and hacl_x5519. Both were one-shot interfaces for a narrow use case (ECDH for NIST P-256 and X25519), worked well for their purpose, and allowed to gather some experience from the development side.

Changed requirements

Revisiting our cryptography stack with the elliptic curve perspective had several reasons, on the one side the customer project NetHSM asked for feasibility of ECDSA/EdDSA for various elliptic curves, on the other side DNSSec uses elliptic curve cryptography (ECDSA), and also wireguard relies on elliptic curve cryptography. The number of X.509 certificates using elliptic curves is increasing, and we don't want to leave our TLS stack in a state where it can barely talk to a growing number of services on the Internet.

Looking at hacl-star, their support is limited to P-256 and Curve25519, any new curve requires writing F*. Another issue with hacl-star is C code quality: their C code does neither compile with older C compilers (found on Oracle Linux 7 / CentOS 7), nor when enabling all warnings (> 150 are generated). We consider the C compiler as useful resource to figure out undefined behaviour (and other problems), and when shipping C code we ensure that it compiles with -Wall -Wextra -Wpedantic --std=c99 -Werror. The hacl project ships a bunch of header files and helper functions to work on all platforms, which is a clunky ifdef desert. The hacl approach is to generate a whole algorithm solution: from arithmetic primitives, group operations, up to cryptographic protocol - everything included.

In contrast, fiat is a Coq development, which as part of compilation (proof verification) generates executables (via OCaml code extraction from Coq). These executables are used to generate modular arithmetic (as C code) given a curve description. The generated C code is highly portable, independent of platform (word size is taken as input) - it only requires a <stdint.h>, and compiles with all warnings enabled (once a minor PR got merged). Supporting a new curve is simple: generate the arithmetic code using fiat with the new curve description. The downside is that group operations and protocol needs to implemented elsewhere (and is not part of the proven code) - gladly this is pretty straightforward to do, especially in high-level languages.

Working with fiat

As mentioned, our initial fiat-p256 binding provided ECDH for the NIST P-256 curve. Also, BoringSSL uses fiat for ECDH, and developed the code for group operations and cryptographic protocol on top of it.

The work needed was (a) ECDSA support and (b) supporting more curves (let's focus on NIST curves). For ECDSA, the algorithm requires modular arithmetics in the field of the group order (in addition to the prime). We generate these primitives with fiat (named npYYY_AA) - that required a small fix in decoding hex. Fiat also provides inversion since late October 2020, paper - which allowed to reduce our code base taken from BoringSSL. The ECDSA protocol was easy to implement in OCaml using the generated arithmetics.

Addressing the issue of more curves was also easy to achieve, the C code (group operations) are macros that are instantiated for each curve - the OCaml code are functors that are applied with each curve description.

Thanks to the test vectors (as structured data) from wycheproof (and again thanks to Etienne, Nathan, and Clément for their OCaml code decodin them), I feel confident that our elliptic curve code works as desired.

What was left is X25519 and Ed25519 - dropping the hacl dependency entirely felt appealing (less C code to maintain from fewer projects). This turned out to require more C code, which we took from BoringSSL. It may be desirable to reduce the imported C code, or to wait until a project on top of fiat which provides proven cryptographic protocols is in a usable state.

To avoid performance degradation, I distilled some X25519 benchmarks, turns out the fiat and hacl performance is very similar.

Achievements

The new opam package mirage-crypto-ec is released, which includes the C code generated by fiat (including inversion), point operations from BoringSSL, and some OCaml code for invoking these functions and doing bounds checks, and whether points are on the curve. The OCaml code are some functors that take the curve description (consisting of parameters, C function names, byte length of value) and provide Diffie-Hellman (Dh) and digital signature algorithm (Dsa) modules. The nonce for ECDSA is computed deterministically, as suggested by RFC 6979, to avoid private key leakage.

The code has been developed in NIST curves, removing blinding (since we use operations that are verified to be constant-time), added missing length checks (reported by Greg), curve25519, a fix for signatures that do not span the entire byte size (discovered while adapting X.509), fix X25519 when the input has offset <> 0. It works on x86 and arm, both 32 and 64 bit (checked by CI). The development was partially sponsored by Nitrokey.

What is left to do, apart from further security reviews, is performance improvements, Ed448/X448 support, and investigating deterministic k for P521. Pull requests are welcome.

When you use the code, and encounter any issues, please report them.

Layer up - X.509 now with ECDSA / EdDSA and PKCS 12 support, and a long-standing issue fixed

With the sign and verify primitives, the next step is to interoperate with other tools that generate and use these public and private keys. This consists of serialisation to and deserialisation from common data formats (ASN.1 DER and PEM encoding), and support for handling X.509 certificates with elliptic curve keys. Since X.509 0.12.0, it supports EC private and public keys, including certificate validation and issuance.

Releasing X.509 also included to go through the issue tracker and attempt to solve the existing issues. This time, the "country name is encoded as UTF8String, while RFC demands PrintableString" filed more than 5 years ago by Reynir, re-reported by Petter in early 2017, and again by Vadim in late 2020, was fixed by Vadim.

Another long-standing pull request was support for PKCS 12, the archive format for certificate and private key bundles. This has been developed and merged. PKCS 12 is a widely used and old format (e.g. when importing / exporting cryptographic material in your browser, used by OpenVPN, ...). Its specification uses RC2 and 3DES (see this nice article), which are the default algorithms used by openssl pkcs12.

One more layer up - TLS

In TLS we are finally able to use ECDSA (and EdDSA) certificates and private keys, this resulted in slightly more complex configuration - the constraints between supported groups, signature algorithms, ciphersuite, and certificates are intricate:

The ciphersuite (in TLS before 1.3) specifies which key exchange mechanism to use, but also which signature algorithm to use (RSA/ECDSA). The supported groups client hello extension specifies which elliptic curves are supported by the client. The signature algorithm hello extension (TLS 1.2 and above) specifies the signature algorithm. In the end, at load time the TLS configuration is validated and groups, ciphersuites, and signature algorithms are condensed depending on configured server certificates. At session initiation time, once the client reports what it supports, these parameters are further cut down to eventually find some suitable cryptographic parameters for this session.

From the user perspective, earlier the certificate bundle and private key was a pair of X509.Certificate.t list and Mirage_crypto_pk.Rsa.priv, now the second part is a X509.Private_key.t - all provided constructors have been updates (notably X509_lwt.private_of_pems and Tls_mirage.X509.certificate).

Finally, conduit and mirage

Thanks to Romain, conduit* 4.0.0 was released which supports the modified API of X.509 and TLS. Romain also developed patches and released mirage 3.10.3 which supports the above mentioned work.

Conclusion

Elliptic curve cryptography is now available in OCaml using verified cryptographic primitives from the fiat project - opam install mirage-crypto-ec. X.509 since 0.12.0 and TLS since 0.13.0 and MirageOS since 3.10.3 support this new development which gives rise to smaller EC keys. Our old bindings, fiat-p256 and hacl_x25519 have been archived and will no longer be maintained.

Thanks to everyone involved on this journey: reporting issues, sponsoring parts of the work, helping with integration, developing initial prototypes, and keep motivating me to continue this until the release is done.

In the future, it may be possible to remove zarith and gmp from the dependency chain, and provide EC-only TLS servers and clients for MirageOS. The benefit will be much less C code (libgmp-freestanding.a is 1.5MB in size) in our trusted code base.

Another potential project that is very close now is a certificate authority developed in MirageOS - now that EC keys, PKCS 12, revocation lists, ... are implemented.

Footer

If you want to support our work on MirageOS unikernels, please donate to robur. I'm interested in feedback, either via twitter, hannesm@mastodon.social or an issue on the data repository.

Have you heard about our Try-Alt-Ergo website? Created in 2014 (see our blogpost), the first objective was to facilitate access to our performant SMT Solver Alt-Ergo. Try-Alt-Ergo allows you to write and run your problems in your browser without any server computation.

This playground website has been maintained by OCamlPro for many years, and it’s high time to bring it back to life with new updates. We are therefore pleased to announce the new version of the Try-Alt-Ergo website! In t…

Have you heard about our Try-Alt-Ergo website? Created in 2014 (see our blogpost), the first objective was to facilitate access to our performant SMT Solver Alt-Ergo. Try-Alt-Ergo allows you to write and run your problems in your browser without any server computation.

This playground website has been maintained by OCamlPro for many years, and it’s high time to bring it back to life with new updates. We are therefore pleased to announce the new version of the Try-Alt-Ergo website! In this article, we will first explain what has changed in the back end, and what you can use if you are interested in running your own version of Alt-Ergo on a website, or in an application! And then we will focus on the new front-end of our website, from its interface to its features through its tutorial about the program.

Try-Alt-Ergo 2014

Try-Alt-Ergo was designed to be a powerful and simple tool to use. Its interface was minimalist. It offered three panels, one panel (left) with a text area containing the problem to prove. The centered panel was composed of a button to run Alt-Ergo, load examples, set options. The right panel showed these options, examples and other information. This design lacked some features that have been added to our solver through the years. Features such as models (counter-examples), unsat-core, more options and debug information was missing in this version.

Try-Alt-Ergo did not offer a proper editor (with syntax coloration), a way to save the file problem nor an option to limit the run of the solver with a time limit. Another issue was about the thread. When the solver was called the webpage froze, that behavior was problematic in case of the long run because there was no way to stop the solver.

Alt-Ergo 1.30

The 1.30 version of Alt-Ergo was the version used in the back-end to prove problems. Since this version, a lot of improvements have been done in Alt-Ergo. To learn more about these improvements, see our changelog in the documentation.

Over the years we encountered some difficulties to update the Alt-Ergo version used in Try-Alt-Ergo. We used Js_of_ocaml to compile the OCaml code of our solver to be runnable as a JavaScript code. Some libraries were not available in JavaScript and we needed to manually disable them. The lack of automatism leads to a lack of time to update the JavaScript version of Alt-Ergo in Try-Alt-Ergo.

In 2019 we switched our build system to dune which opens the possibility to ease the cross-compilation of Alt-Ergo in JavaScript.

New back-end

With some simple modification, we were able to compile Alt-Ergo in JavaScript. This modification is simple enough that this process is now automated in our continuous integration. This will enable us to easily provide a JavaScript version of our Solver for each future version.

Two ways of using our solver in JavaScript are available:

• alt-ergo.js, a JavaScript version of the Alt-Ergo CLI. It can be runned with node: node alt-ergo.js <options> <file>. Note that this code is slower than the natively compiled CLI of Alt-Ergo.
  In our effort to open the SMT world to more people, an npm package is the next steps of this work.
• alt-ergo-worker.js, a web worker of Alt-Ergo. This web worker needs JSON file to input file problem, options into Alt-Ergo and to returns its answers:
  • Options are sent as a list of couple name:value like:
    {"debug":true,
"input_format":"Native",
"steps_bound":100,
"sat_solver": "Tableaux",
"file":"test-file"}
    You can specify all options used in Alt-Ergo. If some options are missing, the worker uses the default value for these options. For example, if debug is not specified the worker will use its defaults value :false.
  • Input file is sent as a list of string, with the following format:
    { "content": [ "goal g: true"] }
  • Alt-Ergo answers can be composed with its results, debug information, errors, warnings …
    { "results": [ "File \"test-file\", line 1, characters 9-13: Valid (0.2070) (0 steps) (goal g) ] ,
"debugs": [ "[Debug][Sat_solver]", "use Tableaux-like solver"] }
    like the options, a result value like debugs does not contains anything, "debugs": [...] is not returned.
  • See the Alt-Ergo web-worker documentation to learn more on how to use it.

New Front-end

The Try-Alt-Ergo has been completely reworked and we added some features:

• The left panel is still composed in an editor and answers area
  • Ace editor with custom syntax coloration (both native and smt-lib2) is now used to make it more pleasant to write your problems.
• A top panel that contains the following buttons:
  • Ask Alt-Ergo which retrieves content from the editor and options, launch the web worker and print answers in the defined areas.
  • Load and Save files.
  • Documentation, that sends users to the newly added native syntax documentation of Alt-Ergo.
  • Tutorial, that opens an interactive tutorial to introduce you to Alt-Ergo native syntax and program verification.
    

• A right panel composed of tabs:
  • Start and About that contains general information about Alt-Ergo, Try-Alt-Ergo and how to use it.
  • Outputs prints more information than the basic answer area under the editor. In these tabs you can find debugs (long) outputs, unsat-core or models (counter-example) generated by Alt-Ergo.
  • Options contains every option you can use, such as the time limit / steps limit or to set the format of the input file to prove .
  • Statistics is still a basic tab that only output axioms used to prove the input problem.
  • Examples contains some basic examples showing the capabilities of our solver.

We hope you will enjoy this new version of Try-Alt-Ergo, we can’t wait to read your feedback!

This work was done at OCamlpro.

About OCamlPro:

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users’ Club). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: contact@ocamlpro.com.

I’ve been running QubesOS as my main desktop since 2015. It provides good security, by running applications in different Xen VMs. However, it is also quite slow and has some hardware problems. I’ve recently been trying out NixOS, KVM, Wayland and SpectrumOS, and attempting to create something similar with more modern/compatible/faster technology.

This post gives my initial impressions of these tools and describes my current setup.

Table of Contents

• QubesOS
• NixOS
  • nix-store

I’ve been running QubesOS as my main desktop since 2015. It provides good security, by running applications in different Xen VMs. However, it is also quite slow and has some hardware problems. I’ve recently been trying out NixOS, KVM, Wayland and SpectrumOS, and attempting to create something similar with more modern/compatible/faster technology.

This post gives my initial impressions of these tools and describes my current setup.

Table of Contents

• QubesOS
• NixOS
  • nix-store
  • nix-instantiate
  • nix-pkgs
  • nix-env
  • NixOS
  • Installing NixOS
  • Thoughts on NixOS
• Why use virtual machines?
• SpectrumOS
• Wayland
  • Protocol
  • Copying text
  • Security
• Future work

( this post also appeared on Hacker News and Lobsters )

QubesOS

QubesOS aims to provide “a reasonably secure operating system”. It does this by running multiple virtual machines under the Xen hypervisor. Each VM’s windows have a different colour and tag, but they appear together as a single desktop. The VMs I run include:

• com for email and similar (the only VM that sees my email password).
• dev for software development.
• shopping (the only VM that sees my card number).
• personal (with no Internet access)
• untrusted (general browsing)

The desktop environment itself is another Linux VM (dom0), used for managing the other VMs. Most of the VMs are running Fedora (the default for Qubes), although I run Debian in dev. There are also a couple of system VMs; one for dealing with the network hardware, and one providing a firewall between the VMs.

You can run qvm-copy in a VM to copy a file to another VM. dom0 pops up a dialog box asking which VM should receive the file, and it arrives there as ~/QubesIncoming/$source_vm/$file. You can also press Ctrl-Shift-C to copy a VM’s clipboard to the global clipboard, and then press Ctrl-Shift-V in a window of the target VM to copy to that VM’s clipboard, ready for pasting into an application.

I think Qubes does a very good job at providing a secure environment.

However, it has poor hardware compatibility and it feels sluggish, even on a powerful machine. I bought a new machine a while ago and found that the motherboard only provided a single video output, limited to 30Hz. This meant I had to buy a discrete graphics card. With the card enabled, the machine fails to resume from suspend, and locks up from time to time (it’s completely stable with the card removed or disabled). I spent some time trying to understand the driver code, but I didn’t know enough about graphics, the Linux kernel, PCI suspend, or Xen to fix it.

I was also having some other problems with QubesOS:

• Graphics performance is terrible (especially on a 4k monitor). Qubes disables graphics acceleration in VMs for security reasons, but it was slow even for software rendering.
• It recently started freezing for a couple of seconds from time to time - annoying when you’re trying to type.
• It uses LVM thin-pools for VM storage, which I don’t understand, and which sometimes need repairing (haven’t lost any data, though).
• dom0 is out-of-date and generally not usable. This is intentional (you should be using VMs), but my security needs aren’t that high and it would be nice to be able to do video conferencing these days. Also, being able to print over USB and use bluetooth would be handy.

Anyway, I decided it was time to try something new. Linux now has its own built-in hypervisor (KVM), and I thought that would probably work better with my hardware. I was also keen to try out Wayland, which is built around shared-memory and I thought it might therefore work better with VMs. How easy would it be to recreate a Qubes-like environment directly on Linux?

NixOS

I’ve been meaning to try NixOS properly for some time. Ever since I started using Linux, its package management has struck me as absurd. On Debian, Fedora, etc, installing a package means letting it put files wherever it likes; which effectively gives the package author root on your system. Not a good base for sandboxing!

Also, they make it difficult to try out 3rd-party software, or to test newer versions of just some packages.

In 2003 I created 0install to address these problems, and Nix has very similar goals. I thought Nix was a few years younger, but looking at its Git history the first commit was on Mar 12, 2003. I announced the first preview of 0install just two days later, so both projects must have started writing code within a few days of each other!

NixOS is made up of quite a few components. Here is what I’ve learned so far:

nix-store

The store holds the files of all the programs, and is the central component of the system. Each version of a package goes in its own directory (or file), at /nix/store/$HASH. You can add data to the store directly, like this:

1
2
3
4
5
6
7

$ echo hello > file

$ nix-store --add-fixed sha256 file
/nix/store/1vap48aqggkk52ijn2prxzxv7cnzvs0w-file

$ cat /nix/store/1vap48aqggkk52ijn2prxzxv7cnzvs0w-file
hello

Here, the store location is calculated from the hash of the contents of the file we added (as with 0install store add or git hash-object).

However, you can also add things to the store by asking Nix to run a build script. For example, to compile some source code:

1. You add the source code and some build instructions (a “derivation” file) to the store.
2. You ask the store to build the derivation. It runs your build script in a container sandbox.
3. The results are added to the store, using the hash of the build instructions (not the hash of the result) as the directory name.

If a package in the store depends on another one (at build time or run time), it just refers to it by its full path. For example, a bash script in the store will start something like:

1
2

#! /nix/store/vnyfysaya7sblgdyvqjkrjbrb0cy11jf-bash-4.4-p23/bin/bash
...

If two users want to use the same build instructions, the second one will see that the hash already exists and can just reuse that. This allows users to compile software from source and share the resulting binaries, without having to trust each other.

Ideally, builds should be reproducible. To encourage this, builds which use the hash of the build instructions for the result path are built in a sandbox without network access. So, you can’t submit a build job like “Download and compile whatever is the latest version of Vim”. But you can discover the latest version yourself and then submit two separate jobs to the store:

1. “Download Vim 8.2, with hash XXX” (a fixed-output job, which therefore has network access)
2. “Build Vim from hash XXX”

You can run nix-collect-garbage to delete everything from the store that isn’t reachable via the symlinks under /nix/var/nix/gcroots/. Users can put symlinks to things they care about keeping in /nix/var/nix/gcroots/per-user/$USER/.

By default, the store is also configured with a trusted binary cache service, and will try to download build results from there instead of compiling locally when possible.

nix-instantiate

Writing derivation files by hand is tedious, so Nix provides a templating language to create them easily. The Nix language is dynamically typed and based around maps/dictionaries (which it confusingly refers to as “sets”). nix-instantiate file.nix will generate a derivation from file.nix and add it to the store.

An Nix file looks like this:

1

derivation { system = "x86_64-linux"; builder = ./myfile; name = "foo"; }

Running nix-instantiate on this will:

1. Add myfile to the store.
2. Add the generated foo.drv to the store, including the full store path of myfile.

nix-pkgs

Writing Nix expressions for every package you want would also be tedious. The nixpkgs Git repository contains a Nix expression that evaluates to a set of derivations, one for each package in the distribution. It also contains a library of useful helper functions for packages (e.g. it knows how to handle GNU autoconf packages automatically).

Rather than evaluating the whole lot, you use -A to ask for a single package. For example, you can use nix-instantiate ./nixpkgs/default.nix -A firefox to generate a derivation for Firefox.

nix-build is a quick way to create a derivation with nix-instantiate and build it with nix-store. It will also create a ./result symlink pointing to its path in the store, as well as registering ./result with the garbage collector under /nix/var/nix/gcroots/auto/. For example, to build and run Firefox:

1
2

nix-build ./nixpkgs/default.nix -A firefox
./result/bin/firefox

If you use nixpkgs without making any changes, it will be able to download a pre-built binary from the cache service.

nix-env

Keeping track of all these symlinks would be tedious too, but you can collect them all together by making a package that depends on every application you want. Its build script will produce a bin directory full of symlinks to the applications. Then you could just point your $PATH variable at that bin directory in the store.

To make updating easier, you will actually add ~/.nix-profile/bin/ to $PATH and update .nix-profile to point at the latest build of your environment package.

This is essentially what nix-env does, except with yet more symlinks to allow for switching between multiple profiles, and to allow rolling back to previous environments if something goes wrong.

For example, to install Firefox so you can run it via $PATH:

1

nix-env -i firefox

NixOS

Finally, just as nix-env can create a user environment with bin, man, etc, a similar process can create a root filesystem for a Linux distribution.

nixos-rebuild reads the /etc/nixos/configuration.nix configuration file, generates a system environment, and then updates grub and the /run/current-system symlink to point to it.

In fact, it also lists previous versions of the system environment in the grub file, so if you mess up the configuration you can just choose an earlier one from the boot menu to return to that version.

Installing NixOS

To install NixOS you boot one of the live images at https://nixos.org. Which you use only affects the installation UI, not the system you end up with.

The manual walks you through the installation process, showing how to partition the disk, format and mount the partitions, and how to edit the configuration file. I like this style of installation, where it teaches you things instead of just doing it for you. Most of the effort in switching to a new system is learning about it, so I’d rather spend 3 hours learning stuff following an installation guide than use a 15-minute single-click installer that teaches me nothing.

The configuration file (/etc/nixos/configuration.nix) is just another Nix expression. Most things are set to off by default (I approve), but can be changed easily. For example, if you want sound support you change that setting to sound.enable = true, and if you also want to use PulseAudio then you set hardware.pulseaudio.enable = true too.

Every system service supported by NixOS is controlled from here, with all kinds of options, from programs.vim.defaultEditor = true (so you don’t get trapped in nano) to services.factorio.autosave-interval. Use man configuration.nix to see the available settings.

NixOS defaults to an X11 desktop, but I wanted to try Wayland (and Sway). Based on the NixOS wiki instructions, I used this:

1
2
3
4
5
6
7
8
9
10
11
12
13
14

  programs.sway = {
    enable = true;
    wrapperFeatures.gtk = true; # so that gtk works properly
    extraSessionCommands = "export MOZ_ENABLE_WAYLAND=1";
    extraPackages = with pkgs; [
      swaylock
      swayidle
      xwayland
      wl-clipboard
      mako
      alacritty
      dmenu
    ];
  };

The xwayland bit is important; without that you can’t run any X11 applications.

My only complaint with the NixOS installation instructions is that following them will leave you with an unencrypted system, which isn’t very useful. When partitioning, you have to skip ahead to the LUKS section of the manual, which just gives some options but no firm advice. I created two primary partitions: a 1G unencrypted /boot, and a LUKS partition for the rest of the disk. Then I created an LVM volume group from the /dev/mapper/crypted device and added the other partitions in that.

Once the partitions are mounted and the configuration file is complete, nixos-install downloads everything and configures grub. Then you reboot into the new system.

Once running the new system you can made further edits to the configuration file there in the same way, and use nixos-rebuild switch to generate a new system. It seems to be pretty good at updating the running system to the new settings, so you don’t normally need to reboot after making changes.

The big mistake I made was forgetting to add /boot to fstab. When I ran nixos-rebuild it put all the grub configuration on the encrypted partition, rendering the system unbootable. I fixed that with chattr +i /boot on the unmounted partition. That way, trying to rebuild with /boot unmounted will just give an error message.

Thoughts on NixOS

I’ve been using the system for a few weeks now and I’ve had no problems with Nix so far. Nix has been fast and reliable and there were fairly up-to-date packages for everything I wanted (I’m using the stable release). There is a lot to learn, but plenty of documentation.

When I wanted a newer package (socat with vsock support, only just released) I just told Nix to install it from the latest Git checkout of nixpkgs. Unlike on Debian and similar systems, doing this doesn’t interfere with any other packages (such as forcing a system-wide upgrade of libc).

I think Nix does download more data than most other systems, but networks are fast enough now that it doesn’t seem to matter. For example, let’s say you’re running Python 3.9.0 and you want to update to 3.9.1:

• With Debian: apt-get upgrade downloads the new version, which gets unpacked over the old one. As the files are unpacked, the system moves through an exciting series of intermediate states no-one has thought about. Running programs may crash as they find their library versions changing under them (though it’s usually OK). Only root can update software.

• With 0install: 0install update downloads the new version, unpacking it to a new directory. Running programs continue to use the old version. When a new program is started, 0install notices the update and runs the solver again. If the program is compatible with the new Python then it uses that. If not, it continues with the old one. You can run any previous version if there is a problem.

• With Nix: nix-env -u downloads the new version, unpacking it to a new directory. It also downloads (or rebuilds) every package depending on Python, creating new directories for each of them. It then creates a new environment with symlinks to the latest version of everything. Running programs continue to use the old version. Starting a new program will use the new version. You can revert the whole environment back to the previous version if there is a problem.

• With Docker: docker pull downloads the new version of a single application, downloading most or all of the application’s packages, whether Python related or not. Existing containers continue running with the old version. New containers will default to using the new version. You can specify which version to use when starting a program. Other applications continue using the old version of Python until their authors update them (you must update each application individually, rather than just updating Python itself).

The main problem with NixOS is that it’s quite different to other Linux systems, so there’s a lot to relearn. Also, existing knowledge about how to edit fstab, sudoers, etc, isn’t so useful, as you have to provide all configuration in Nix syntax. However, having a single (fairly sane) syntax for everything is a nice bonus, and being able to generate things using the templating language is useful. For example, for my network setup I use a bunch of tap devices (one for each of my VMs). It was easy to write a little Nix function (mktap) to generate them all from a simple list. Here’s that section of my configuration.nix:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

  networking = {
    useDHCP = false;
    interfaces =
      let mktap = ip: {
          virtual = true;
          virtualOwner = "tal";
          ipv4.addresses = [
            { address = ip; prefixLength = 31; }
          ];
        };
      in
      {
        eno2.useDHCP = true;
        wlo1.useDHCP = true;
        tapdev = mktap "10.0.0.2";
        tapcom = mktap "10.0.0.4";
        tapshopping = mktap "10.0.0.6";
        tapbanking = mktap "10.0.0.8";
        tapuntrusted = mktap "10.0.0.10";
      };
    nat = {
      enable = true;
      externalInterface = "eno2";
      internalIPs = [ "10.0.0.0/8" ];
    };
  };

Overall, I’m very happy with NixOS so far.

Why use virtual machines?

With NixOS I had a nice host environment, but after using Qubes I wanted to run my applications in VMs.

The basic problem is that Linux is the only thing that knows how to drive all the hardware, but Linux security is not ideal. There are several problems:

1. Linux is written in C. This makes security bugs rather common and, more importantly, means that a bug in one part of the code can impact any other part of the code. Nothing is secure unless everything is secure.
2. Linux has a rather large API (hundreds of syscalls).
3. The Linux (Unix) design predates the Internet, and security has been somewhat bolted on afterwards.

For example, imagine that we want to run a program with access to the network, but not to the graphical display. We can create a new Linux container for it using bubblewrap, like this:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

$ ls -l /run/user/1000/wayland-0 /tmp/.X11-unix/X0
srwxr-xr-x 1 tal users 0 Feb 18 16:41 /run/user/1000/wayland-0
srwxr-xr-x 1 tal users 0 Feb 18 16:41 /tmp/.X11-unix/X0

$ bwrap \
    --ro-bind / / \
    --dev /dev \
    --tmpfs /home/tal \
    --tmpfs /run/user \
    --tmpfs /tmp \
    --unshare-all --share-net \
    bash

$ ls -l /run/user/1000/wayland-0 /tmp/.X11-unix/X0
ls: cannot access '/run/user/1000/wayland-0': No such file or directory
ls: cannot access '/tmp/.X11-unix/X0': No such file or directory

The container has an empty home directory, empty /tmp, and no access to the display sockets. If we run Firefox in this environment then… it opens its window just fine! How? strace shows what happened:

1
2
3

connect(4, {sa_family=AF_UNIX, sun_path="/run/user/1000/wayland-0"}, 27) = -1 ENOENT (No such file or directory)
socket(AF_UNIX, SOCK_STREAM|SOCK_CLOEXEC, 0) = 4
connect(4, {sa_family=AF_UNIX, sun_path=@"/tmp/.X11-unix/X0"}, 20) = 0

After failing to connect to Wayland, it then tried using X11 (via Xwayland) instead. Why did that work? If the first byte of the socket pathname is \0 then Linux instead interprets it as an “abstract” socket address, not subject to the usual filesystem permission rules.

Trying to anticipate these kinds of special cases is just too much work. Linux really wants everything on by default, and you have to find and disable every feature individually. By contrast, virtual machines tend to have integrations with the host off by default. The also tend to have much smaller APIs (e.g. just reading and writing disk blocks or network frames), with the rich Unix API entirely inside the VM, provided by a separate instance of Linux.

SpectrumOS

I was able to set up a qemu guest and restore my dev Qubes VM in that, but it didn’t integrate nicely with the rest of the desktop. Installing ssh allowed me to connect in with ssh -Y dev, allowing apps in the VM to open an X connection to Xwayland on the host. That was somewhat usable, but still a bit slower than Qubes had been (which was already a bit too slow).

Searching for a way to forward the Wayland connection directly, I came across the SpectrumOS project. SpectrumOS aims to use one virtual machine per application, using shared directories so that VM files are stored on the host, simplifying management. It uses crosvm from the ChromiumOS project instead of qemu, because it has a driver that allows forwarding Wayland connections (and also because it’s written in Rust rather than C). The project’s single developer is currently taking a break from the project, and says “I’m currently working towards a proof of concept”.

However, there is some useful stuff in the SpectrumOS repository (which is a fork of nixpkgs). In particular, it contains:

• A version of Linux with the virtwl kernel module, which connects to crosvm’s Wayland driver.
• A package for sommelier, which connects applications to virtwl.
• A Nix expression to build a root filesystem for the VM.

Building that, I was able to run the project’s demo, which runs the Wayfire compositor inside the VM, appearing in a window on the host. Dragging the nested window around, the pixels flowed smoothly across my screen in exactly the way that pixels on QubesOS don’t.

This was encouraging, but I didn’t want to run a nested window manager. I tried running Firefox directly (without Wayfire), but it complained that sommelier didn’t provide a new enough version of something, and running weston-terminal immediately segfaulted sommelier.

Why do we need the sommelier process anyway? The problem is that, while virtwl mostly proxies Wayland messages directly, it can’t send arbitrary FDs to the host. For example, if you want to forward a writable stream from an application to virtwl you must first create a pipe from the host using a special virtwl ioctl, then read from that and copy the data to the application’s regular Linux pipe.

With help from the mailing list, I managed to get it somewhat usable:

• I enabled VIRTIO_FS, allowing me to mount a host directory into the VM (for sharing files).
• I created some tap devices (as mentioned above) to get guest networking going.
• Adding ext4 to the kernel image allowed me to mount the VM’s LVM partition.
• Setting FONTCONFIG_FILE got some usable fonts (otherwise, there was no monospace font for the terminal).
• I hacked sommelier to claim it supported the latest protocols, which got Firefox running.
• Configuring sommelier for Xwayland let X applications run.
• I replaced the non-interactive bash shell with fish so I could edit commands.
• I ran (while true; do socat vsock-listen:5000 exec:dash; done) at the end of the VM’s boot script. Then I could start e.g. the VM’s Firefox with echo 'firefox&' | socat stdin vsock-connect:7:5000 on the host, allowing me to add launchers for guest applications.

Making changes to the root filesystem was fairly easy once I’d read the Nix manuals. To add an application (e.g. libreoffice), you import it at the start of rootfs/default.nix and add it to the path variable. The Nix expression gets the transitive dependencies of path from the Nix store and packs them into a squashfs image.

True, my squashfs image is getting a bit big. Maybe I should instead make a minimal squashfs boot image, plus a shared directory of hard links to the required files. That would allow sharing the data with the host. I could also just share the whole /nix/store directory, if I wanted to make all host software available to guests.

I made another Nix script to add various VM boot commands to my host environment. For example, running qvm-start-shopping boots my shopping VM using crosvm, with the appropriate LVM data partition, network settings, and shared host directory.

I think, ideally, this would be a systemd socket-activated user service rather than a shell script. Then attempting to run Firefox by sending a command to the VM socket would cause systemd to boot the VM (if not already running). For now, I boot each VM manually in a terminal and then press Win-Shift-2 to banish it to workspace 2, with all the other VM root consoles.

The virlwl Wayland forwarding feels pretty fast (much faster than Qubes’ X graphics).

Wayland

I now had a mostly functional Qubes-like environment, running most of my applications in VMs, with their windows appearing on the host desktop like any other application. However, I also had some problems:

• A stated goal of Wayland is “every frame is perfect”. However, applications generally seemed to open at the wrong size and then jump to their correct size, which was a bit jarring.
• Vim opened its window with the scrollbar at the far left of the window, making the text invisible until you resized the window.
• Wayland is supposed to have better support for high-DPI displays. However, this doesn’t work with Xwayland, which turns everything blurry, and the recommended work-around is to use a scale-factor of 1 and configure each application to use bigger fonts. This is easy enough with X applications (e.g. set ft.dpi: 150 with xrdb), but Wayland apps must be configured individually.
• Wayland doesn’t have cursor themes and you have to configure every application individually to use a larger cursor too.
• Copying text didn’t seem to work reliably. Sometimes there would be a long delay, after which the text might or might not appear. More often, it would just paste something completely different and unexpected. Even when it did paste the right text, it would often have ^M characters inserted into it.

I decided it was time to learn more about Wayland. I discovered wayland-book.com, which does a good job of introducing it (though the book is only half finished at the moment).

Protocol

One very nice feature of Wayland is that you can run any Wayland application with WAYLAND_DEBUG=1 and it will display a fairly readable trace of all the Wayland messages it sends and receives. Let’s look at a simple application that just connects to the server (compositor) and opens a window:

1
2
3

$ WAYLAND_DEBUG=1 test.exe
-> wl_display@1.get_registry registry:+2
-> wl_display@1.sync callback:+3

The client connects to the server’s socket at /run/user/1000/wayland-0 and sends two messages to object 1 (of type wl_display), which is the only object available in a new connection. The get_registry request asks the server to add the registry to the conversation and call it object 2. The sync request just asks the server to confirm it got it, using a new callback object (with ID 3).

Both clients and servers can add objects to the conversation. To avoid numbering conflicts, clients assign low numbers and servers pick high ones.

On the wire, each message gives the object ID, the operation ID, the length in bytes, and then the arguments. Objects are thought of as being at server, so the client sends request messages to objects, while the server emits event messages from objects. At the wire level there’s no difference though.

When the server gets the get_registry request it adds the registry, which immediately emits one event for each available service, giving the maximum supported version. The client receives these messages, followed by the callback notification from the sync message:

1
2
3
4
5
6
7
8
9
10

<- wl_registry@2.global name:0 interface:"wl_compositor" version:4
<- wl_registry@2.global name:1 interface:"wl_subcompositor" version:1
<- wl_registry@2.global name:2 interface:"wl_shm" version:1
<- wl_registry@2.global name:3 interface:"xdg_wm_base" version:1
<- wl_registry@2.global name:4 interface:"wl_output" version:2
<- wl_registry@2.global name:5 interface:"wl_data_device_manager" version:3
<- wl_registry@2.global name:6 interface:"zxdg_output_manager_v1" version:3
<- wl_registry@2.global name:7 interface:"gtk_primary_selection_device_manager" version:1
<- wl_registry@2.global name:8 interface:"wl_seat" version:5
<- wl_callback@3.done callback_data:1129040

The callback tells the client it has seen all the available services, and so it now picks the ones it wants. It has to choose a version no higher than the one offered by the server. Protocols starting with wl_ are from of the core Wayland protocol; the others are extensions. The leading z in zxdg_output_manager_v1 indicates that the protocol is “unstable” (under development).

The protocols are defined in various XML files, which are scattered over the web. The core protocol is defined in wayland.xml. These XML files can be used to generate typed bindings for your programming language of choice.

Here, the application picks wl_compositor (for managing drawing surfaces), wl_shm (for sharing memory with the server), and xdg_wm_base (for desktop windows).

1
2
3

-> wl_registry@2.bind name:0 id:+4(wl_compositor:v4)
-> wl_registry@2.bind name:2 id:+5(wl_shm:v1)
-> wl_registry@2.bind name:3 id:+6(xdg_wm_base:v1)

The bind message is unusual in that the client gives the interface and version of the object it is creating. For other messages, both sides know the type from the schema, and the version is always the same as the parent object. Because the client chose the new IDs, it doesn’t need to wait for the server; it continues by using the new objects to create a top-level window:

1
2
3
4
5

-> wl_compositor@4.create_surface id:+7
-> xdg_wm_base@6.get_xdg_surface id:+8 surface:7
-> xdg_surface@8.get_toplevel id:+9
-> xdg_toplevel@9.set_title title:"example app"
-> wl_surface@7.commit 

This API is pretty strange. The core Wayland protocol says how to make generic drawing surfaces, but not how to make windows, so the application is using the xdg_wm_base extension to do that. Logically, there’s only one object here (a toplevel window), but it ends up making three separate Wayland objects representing the different aspects of it.

The commit tells the server that the client has finished setting up the window and the server should now do something with it.

The above was all in response to the callback firing. The client now processes the last message in that batch, which is the server destroying the callback:

1

<- wl_display@1.delete_id id:3

Object destruction is a bit strange in Wayland. Normally, clients ask for things to be destroyed (by sending a “destructor” message) and the server confirms by sending delete_id from object 1. But this isn’t symmetrical: there is no standard way for a client to confirm deletion when the server calls a destructor (such as the callback’s done), so these have to be handled on a case-by-case basis. Since callbacks don’t accept any messages, there is no need for the client to confirm that it got the done message and the server just sends a delete message immediately.

The client now waits for the server to respond to all the messages it sent about the new window, and gets a bunch of replies:

1
2
3
4
5
6
7
8
9

<- wl_shm@5.format format:0
<- wl_shm@5.format format:1
<- wl_shm@5.format format:875709016
<- wl_shm@5.format format:875708993
<- xdg_wm_base@6.ping serial:1129043
-> xdg_wm_base@6.pong serial:1129043
<- xdg_toplevel@9.configure width:0 height:0 states:""
<- xdg_surface@8.configure serial:1129042
-> xdg_surface@8.ack_configure serial:1129042

It gets some messages telling it what pixel formats are supported, a ping message (which the server sends from time to time to check the client is still alive), and a configure message giving the size for the new window. Oddly, Sway has set the size to 0x0, which means the client should choose whatever size it likes.

The client picks a suitable default size, allocates some shared memory (by opening a tmpfs file and immediately unlinking it), shares the file descriptor with the server (create_pool), and then carves out a portion of the memory to use as a buffer for the pixel data:

1
2
3

-> wl_shm@5.create_pool id:+3 fd:(fd) size:1228800
-> wl_shm_pool@3.create_buffer id:+10 offset:0 width:640 height:480 stride:2560 format:1
-> wl_shm_pool@3.destroy 

In this case it used the whole memory region. It could also have allocated two buffers for double-buffering. The client then draws whatever it wants into the buffer (mapping the file into its memory and writing to it directly), attaches the buffer to the window’s surface, marks the whole area as “damaged” (in need of being redrawn) and calls commit, telling the server the surface is ready for display:

1
2
3

-> wl_surface@7.attach buffer:10 x:0 y:0
-> wl_surface@7.damage x:0 y:0 width:2147483647 height:2147483647
-> wl_surface@7.commit 

At this point the window appears on the screen! The server lets the client know it has finished with the buffer and the client destroys it:

1
2
3

<- wl_display@1.delete_id id:3
<- wl_buffer@10.release 
-> wl_buffer@10.destroy 

Although the window is visible, the content is the wrong size. Sway now suddenly remembers that it’s a tiling window manager. It sends another configure event with the correct size, causing the client to allocate a fresh memory pool of the correct size, allocate a fresh buffer from it, redraw everything at the new size, and tell the server to draw it.

1
2

<- xdg_toplevel@9.configure width:1534 height:1029 states:""
...

This process of telling the client to pick a size and then overruling it explains why Firefox draws itself incorrectly at first and then flickers into position a moment later. It probably also explains why Vim tries to open a 0x0 window.

Copying text

A bit of searching revealed that the ^M problem is a known Sway bug.

However, the main reason copying text wasn’t working turned out to be a limitation in the design of the core wl_data_device_manager protocol. The normal way to copy text on X11 is to select the text you want to copy, then click the middle mouse button where you want it (or press Shift-Insert).

X also supports a clipboard mechanism, where you select text, then press Ctrl-C, then click at the destination, then press Ctrl-V. The original Wayland protocol only supports the clipboard system, not the selection, and so Wayland compositors have added selection support through extensions. Sommelier didn’t proxy these extensions, leading to failure when copying in or out of VMs.

I also found that the reason weston-terminal wouldn’t start was because I didn’t have anything in my clipboard, and sommelier was trying to dereference a null pointer.

One problem with the Wayland protocol is that it’s very hard to proxy. Although the wire protocol gives the length in bytes of each message, it doesn’t say how many file descriptors it has. This means that you can’t just pass through messages you don’t understand, because you don’t know which FDs go with which message. Also, the wire protocol doesn’t give types for FDs (nor does the schema), which is a problem for anything that needs to proxy across a VM boundary or over a network.

This all meant that VMs could only use protocols explicitly supported by sommelier, and sommelier limited the version too. Which means that supporting extra extensions or new versions means writing (and debugging) loads of C++ code.

I didn’t have time to write and debug C++ code for every missing Wayland protocol, so I took a short-cut: I wrote my own Wayland library, ocaml-wayland, and then used that to write my own version of sommelier. With that, adding support for copying text was fairly easy.

For each Wayland interface we need to handle each incoming message from the client and forward it to the host, and also forward each message from the host to the client. Here’s the code to handle the “selection” event in OCaml, which we receive from the host and send to the client (c):

1

method on_selection _ offer = C.Wl_data_device.selection c (Option.map to_client offer)

The host passes us an “offer” argument, which is a previously-created host offer object. We look up the corresponding client object with to_client and pass that as the argument to the client.

For comparison, here’s sommelier’s equivalent to this line of code, in C++:

1
2
3
4
5
6
7
8
9
10

static void sl_data_device_selection(void* data,
                                     struct wl_data_device* data_device,
                                     struct wl_data_offer* data_offer) {
  struct sl_host_data_device* host = static_cast<sl_host_data_device*>(
      wl_data_device_get_user_data(data_device));
  struct sl_host_data_offer* host_data_offer =
      static_cast<sl_host_data_offer*>(wl_data_offer_get_user_data(data_offer));

  wl_data_device_send_selection(host->resource, host_data_offer->resource);
}

I think this is a great demonstration of the difference between “type safety” and “type ceremony”. The C++ code is covered in types, making the code very hard to read, yet it crashes at runtime because it fails to consider that data_offer can be NULL.

By contract, the OCaml version has no type annotations, but the compiler would reject if I forgot to handle this (with Option.map).

Security

According to the GNOME wiki, the original justification for not supporting selection copies was “security concerns with unexpected data stealing if the mere act of selecting a text fragment makes it available to all running applications”. The implication is that applications stealing data instead from the clipboard is OK, and that you should therefore never put anything confidential on the clipboard.

This seemed a bit odd, so I read the security section of the Wayland specification to learn more about its security model. That section of the specification is fairly short, so I’ll reproduce it here in full:

Security and Authentication

• mostly about access to underlying buffers, need new drm auth mechanism (the grant-to ioctl idea), need to check the cmd stream?
• getting the server socket depends on the compositor type, could be a system wide name, through fd passing on the session dbus. or the client is forked by the compositor and the fd is already opened.

It looks like implementations have to figure things out for themselves.

The main advantage of Wayland over X11 here is that Wayland mostly isolates applications from each other. In X11 applications collaborate together to manage a tree of windows, and any application can access any window. In the Wayland protocol, each application’s connection only includes that application’s objects. Applications only get events relevant to their own windows (for example, you only get pointer motion events while the pointer is over your window). Communication between applications (e.g. copy-and-paste or drag-and-drop) is all handled though the compositor.

Also, to request the contents of the clipboard you need to quote the serial number of the mouse click or key press that triggered it. If it’s too far in the past, the compositor can ignore the request.

I’ve also heard people say that security is the reason you can’t take screenshots with Wayland. However, Sway lets you take screenshots, and this worked even from inside a VM through virtwl. I didn’t add screenshot support to the proxy, because I don’t want VMs to be able to take screenshots, but the proxy isn’t a security tool (it runs inside the VM, which isn’t trusted).

Clearly, the way to fix this was with a new compositor. One that would offer a different Wayland socket to each VM, tag the windows with the VM name, colour the frames, confirm copies across VM boundaries, and work with Vim. Luckily, I already had a handy pure-OCaml Wayland protocol library available. Unluckily, at this point I ran out of holiday.

Future work

There are quite a few things left to do here:

• One problem with virtwl is that, while we can receive shared memory FDs from the host, we can’t export guest memory to the host. This is unfortunate, because in Wayland the shared memory for window contents is allocated by the application from guest memory, and the proxy therefore has to copy each frame. If the host provided the memory to the guest, this wouldn’t be needed. There is a wl_drm protocol for allocating video memory, which might help here, but I don’t know how that works and, like many Wayland specifications, it seems to be in the process of being replaced by something else. Also, if we’re going to copy the memory, we should at least only copy the damaged region, not the whole thing. I only got this code working just far enough to run the Wayland applications I use (mainly Firefox and Evince).

• I’m still using ssh to proxy X11 connections (mainly for Vim and gitk). I’d prefer to run Xwayland in the VM, but it seems you need to provide a bit of extra support for that, which I haven’t implemented yet. Sommelier can do this, but then copying doesn’t work.

• The host Wayland compositor needs to be aware of VMs, so it can colour the titles appropriately and limit access to privileged operations.

• For the full Qubes experience, the network card should be handled by a VM, with another VM managing the firewall. Perhaps the Mirage unikernel firewall could be made to work on KVM too. I’m not sure how guest-to-guest communication works with KVM.

However, because the host NixOS environment is a fully-working Linux system, I can always trade off some security to get things working (e.g. by doing video conferencing directly on the host).

I hope the SpectrumOS project will resume at some point, or that Qubes will find a solution to its hardware compatibility and performance problems.

In collaboration with Nomadic Labs, Marigold and DaiLambda, we're happy to announce the completion of the next Tezos protocol proposal: Florence.

Tezos is an open-source decentralised blockchain network providing a platform for smart contracts and digital assets. A crucial feature of Tezos is self-amendment: the network protocol can be upgraded dynamically by the network participants themselves. This amendment process is initiated when a participant makes a proposal, which is then subject to a v…

In collaboration with Nomadic Labs, Marigold and DaiLambda, we're happy to announce the completion of the next Tezos protocol proposal: Florence.

Tezos is an open-source decentralised blockchain network providing a platform for smart contracts and digital assets. A crucial feature of Tezos is self-amendment: the network protocol can be upgraded dynamically by the network participants themselves. This amendment process is initiated when a participant makes a proposal, which is then subject to a vote. After several years working on the Tezos storage stack, this is our first contribution to a proposal; we hope that it will be the first of many!

As detailed in today's announcement from Nomadic Labs, the Florence proposal contains several important changes, from the introduction of Baking Accounts to major quality-of-life improvements for smart contract developers. Of all of these changes, we're especially excited about the introduction of sub-trees to the blockchain context API. In this post, we'll give a brief tour of what these sub-trees will bring for the future of Tezos. But first, what are they?

Merkle sub-trees

The Tezos protocol runs on top of a versioned tree called the “context”, which holds the chain state (balances, contracts etc.). Ever since the pre-Alpha era, the Tezos context has been implemented using Irmin – an open-source Merkle tree database originally written for use by MirageOS unikernels.

For MirageOS, Irmin’s key strength is flexibility: it can run over arbitrary backends. This is a perfect fit for Tezos, which must be agile and widely-deployable. Indeed, the Tezos shell has already leveraged this agility many times, all the way from initial prototypes using a Git backend to the optimised irmin-pack implementation used today.

But Irmin can do more than just swapping backends! It also allows users to manipulate the underlying Merkle tree structure of the store with a high-level API. This “Tree” API enables lots of interesting use-cases of Irmin, from mergeable data types (MRDTs) to zero-knowledge proofs. Tezos doesn't use these more powerful features directly yet; that’s where Merkle proofs come in!

Proofs and lightweight Tezos clients

Since the Tezos context keeps track of the current "state" of the blockchain, each participant needs their own copy of the tree to run transactions against. This context can grow to be very large, so it's important that it be stored as compactly as possible: this goal shaped the design of irmin-pack, our latest Irmin backend.

However, it's possible to reduce the storage requirements even further via the magic of Merkle trees: individuals only need to store a fragment of the root tree, provided they can demonstrate that this fragment is valid by sending “proofs” of its membership to the other participants.

This property can be used to support ultra-lightweight Tezos clients, a feature currently being developed by TweagIO. To make this a reality, the Tezos protocol needs fine-grained access to context sub-trees in order build Merkle proofs out of them. Fortunately, Irmin already supports this! We extended the protocol to understand sub-trees, lifting the power of Merkle trees to the user.

We’re excited to work with TweagIO and Nomadic Labs on lowering the barriers to entering the Tezos ecosystem and look forward to seeing what they achieve with sub-trees!

Efficient Merkle proof representations

Simply exposing sub-trees in the Tezos context API isn’t quite enough: lightweight clients will also need to serialize them efficiently, since proofs must be exchanged over the network to establish trust between collaborating nodes. Enter Plebeia.

Plebeia is an alternative Tezos storage layer – developed by DaiLambda – with strengths that complement those of Irmin. In particular, Plebeia is capable of generating very compact Merkle proofs. This is partly due to its specialized store structure, and partly due to clever optimizations such as path compression and inlining.

We’re working with the DaiLambda team to unite the strengths of Irmin and Plebeia, which will bring built-in Merkle proof support to the Tezos storage stack. The future is bright for Merkle proofs in Tezos!

Baking account migrations

Trees don’t just enable new features; they have a big impact on performance too! Currently, indexing into the context always happens from its root, which duplicates effort when accessing adjacent values deep in the tree. Fortunately, the new sub-trees provide a natural representation for “cursors” into the context, allowing the protocol to optimize its interactions with the storage layer.

To take just one example, DaiLambda recently exploited this feature to reduce the migration time necessary to introduce Baking Accounts to the network by a factor of 15! We’ll be teaming up with Nomadic Labs and DaiLambda to ensure that Tezos extracts every bit of performance from its storage.

It's especially exciting to have access to lightning-fast storage migrations, since this enables Tezos to evolve rapidly even as the ecosystem expands.

Storage in other languages

Of course, Tezos isn’t just an OCaml project: the storage layer also has a performant Rust implementation as part of TezEdge. We’re working with Simple Staking to bring Irmin to the Rust community via an FFI toolchain, enabling closer alignment between the different Tezos shell implementations.

Conclusion

All in all, it’s an exciting time to work on Tezos storage, with many open-source collaborators from around the world. We’re especially happy to see Tezos taking greater advantage of Irmin’s features, which will strengthen both projects and help them grow together.

If all of this sounds interesting, you can play with it yourself using the recently-released Irmin 2.5.0. Thanks for reading, and stay tuned for future Tezos development updates!

The Coq development team is proud to announce the immediate availability of the Coq Platform 2021.02.0

The Coq platform is a distribution of the Coq proof assistant together with a selection of Coq libraries. It provides a set of scripts to compile and install OPAM, Coq, Coq libraries and Coq plugins on MacOS, Windows and many Linux distributions in a reliable way with consistent results.

This release is based on Coq 8.13.1 and provides binary installers for Windows and Linux. We plan t…

The Coq development team is proud to announce the immediate availability of the Coq Platform 2021.02.0

The Coq platform is a distribution of the Coq proof assistant together with a selection of Coq libraries. It provides a set of scripts to compile and install OPAM, Coq, Coq libraries and Coq plugins on MacOS, Windows and many Linux distributions in a reliable way with consistent results.

This release is based on Coq 8.13.1 and provides binary installers for Windows and Linux. We plan to release 2021.02.1 as soon as the MacOS installer is ready. The following point releases, starting with 2021.02.2, will focus on including more Coq libraries (and no breaking change).

This is joint work with Marc Bezem, Thierry Coquand, Peter Dybjer.

We use the Burali-Forti argument to show that, in homotopy type theory and univalent foundations, the embedding $$ \mathcal{U} \to \mathcal{U}^+$$ of a universe $\mathcal{U}$ into its successor $\mathcal{U}^+$ is not an equivalence. We also establish this for the types of sets, magmas, monoids and groups. The arguments in this post are also written in Agda.

Ordinals in univalent type theory

The Burali-Forti paradox is about…

This is joint work with Marc Bezem, Thierry Coquand, Peter Dybjer.

We use the Burali-Forti argument to show that, in homotopy type theory and univalent foundations, the embedding $$ \mathcal{U} \to \mathcal{U}^+$$ of a universe $\mathcal{U}$ into its successor $\mathcal{U}^+$ is not an equivalence. We also establish this for the types of sets, magmas, monoids and groups. The arguments in this post are also written in Agda.

Ordinals in univalent type theory

The Burali-Forti paradox is about the collection of all ordinals. In set theory, this collection cannot be a set, because it is too big, and this is what the Burali-Forti argument shows. This collection is a proper class in set theory.

In univalent type theory, we can collect all ordinals of a universe $\mathcal{U}$ in a type $\operatorname{Ordinal}\,\mathcal{U}$ that lives in the successor universe $\mathcal{U}^+$: $$ \operatorname{Ordinal}\,\mathcal{U} : \mathcal{U}^+.$$ See Chapter 10.3 of the HoTT book, which uses univalence to show that this type is a set in the sense of univalent foundations (meaning that its equality is proposition valued).

The analogue in type theory of the notion of proper class in set theory is that of large type, that is, a type in a successor universe $\mathcal{U}^+$ that doesn't have a copy in the universe $\mathcal{U}$. In this post we show that the type of ordinals is large and derive some consequences from this.

We have two further uses of univalence, at least:

1. to adapt the Burali-Forti argument from set theory to our type theory, and

2. to resize down the values of the order relation of the ordinal of ordinals, to conclude that the ordinal of ordinals is large.

There are also a number of uses of univalence via functional and propositional extensionality.

Propositional resizing rules or axioms are not needed, thanks to (2).

An ordinal in a universe $\mathcal{U}$ is a type $X : \mathcal{U}$ equipped with a relation $$ - \prec - : X \to X \to \mathcal{U}$$

required to be

1. proposition valued,

2. transitive,

3. extensional (any two points with same lower set are the same),

4. well founded (every element is accessible, or, equivalently, the principle of transfinite induction holds).

The HoTT book additionally requires $X$ to be a set, but this follows automatically from the above requirements for the order.

The underlying type of an ordinal $\alpha$ is denoted by $\langle \alpha \rangle$ and its order relation is denoted by $\prec_{\alpha}$ or simply $\prec$ when we believe the reader will be able to infer the missing subscript.

Equivalence of ordinals in universes $\mathcal{U}$ and $\mathcal{V}$, $$ -\simeq_o- : \operatorname{Ordinal}\,\mathcal{U} \to \operatorname{Ordinal}\,\mathcal{V} \to \mathcal{U} \sqcup \mathcal{V},$$ means that there is an equivalence of the underlying types that preserves and reflects order. Here we denote by $\mathcal{U} \sqcup \mathcal{V}$ the least upper bound of the two universes $\mathcal{U}$ and $\mathcal{V}$. The precise definition of the type theory we adopt here, including the handling of universes, can be found in Section 2 of this paper and also in our Midlands Graduate School 2019 lecture notes in Agda form.

For ordinals $\alpha$ and $\beta$ in the same universe, their identity type $\alpha = \beta$ is canonically equivalent to the ordinal-equivalence type $\alpha \simeq_o \beta$, by univalence.

The lower set of a point $x : \langle \alpha \rangle$ is written $\alpha \downarrow x$, and is itself an ordinal under the inherited order. The ordinals in a universe $\mathcal{U}$ form an ordinal in the successor universe $\mathcal{U}^+$, denoted by $$ \operatorname{OO}\,\mathcal{U} : \operatorname{Ordinal}\,\mathcal{U}^+,$$ for ordinal of ordinals.

Its underlying type is $\operatorname{Ordinal}\,\mathcal{U}$ and its order relation is denoted by $-\triangleleft-$ and is defined by $$\alpha \triangleleft \beta = \Sigma b : \langle \beta \rangle , \alpha = (\beta \downarrow b).$$

This order has type $$-\triangleleft- : \operatorname{Ordinal}\,\mathcal{U} \to \operatorname{Ordinal}\,\mathcal{U} \to \mathcal{U}^+,$$ as required for it to make the type $\operatorname{\operatorname{Ordinal}} \mathcal{U}$ into an ordinal in the next universe.

By univalence, this order is equivalent to the order defined by $$\alpha \triangleleft^- \beta = \Sigma b : \langle \beta \rangle , \alpha \simeq_o (\beta \downarrow b).$$ This has the more general type $$ -\triangleleft^-- : \operatorname{\operatorname{Ordinal}}\,\mathcal{U} \to \operatorname{\operatorname{Ordinal}}\,\mathcal{V} \to \mathcal{U} \sqcup \mathcal{V},$$ so that we can compare ordinals in different universes. But also when the universes $\mathcal{U}$ and $\mathcal{V}$ are the same, this order has values in $\mathcal{U}$ rather than $\mathcal{U}^+$. The existence of such a resized-down order is crucial for our corollaries of Burali-Forti, but not for Burali-Forti itself.

For any $\alpha : \operatorname{Ordinal}\,\mathcal{U}$ we have $$ \alpha \simeq_o (\operatorname{OO}\,\mathcal{U} \downarrow \alpha),$$ so that $\alpha$ is an initial segment of the ordinal of ordinals, and hence $$ \alpha \triangleleft^- \operatorname{OO}\,\mathcal{U}.$$

The Burali-Forti theorem in HoTT/UF

We adapt the original formulation and argument from set theory.

Theorem. No ordinal in a universe $\mathcal{U}$ can be equivalent to the ordinal of all ordinals in $\mathcal{U}$.

Proof. Suppose, for the sake of deriving absurdity, that there is an ordinal $\alpha \simeq_o \operatorname{OO}\,\mathcal{U}$ in the universe $\mathcal{U}$. By the above discussion, $\alpha \simeq_o \operatorname{OO}\,\mathcal{U} \downarrow \alpha$, and, hence, by symmetry and transitivity, $\operatorname{OO}\,\mathcal{U} \simeq_o \operatorname{OO}\,\mathcal{U} \downarrow \alpha$. Therefore, by univalence, $\operatorname{OO}\,\mathcal{U} = \operatorname{OO}\,\mathcal{U} \downarrow \alpha$. But this means that $\operatorname{OO}\,\mathcal{U} \triangleleft \operatorname{OO}\,\mathcal{U}$, which is impossible as any accessible relation is irreflexive. $\square$

Some corollaries follow.

The type of ordinals is large

We say that a type in the successor universe $\mathcal{U}^+$ is small if it is equivalent to some type in the universe $\mathcal{U}$, and large otherwise.

Theorem. The type of ordinals of any universe is large.

Proof. Suppose the type of ordinals in the universe $\mathcal{U}$ is small, so that there is a type $X : \mathcal{U}$ equivalent to the type $\operatorname{Ordinal}\, \mathcal{U} : \mathcal{U}^+$. We can then transport the ordinal structure from the type $\operatorname{Ordinal}\, \mathcal{U}$ to $X$ along this equivalence to get an ordinal in $\mathcal{U}$ equivalent to the ordinal of ordinals in $\mathcal{U}$, which is impossible by the Burali-Forti theorem.

But the proof is not concluded yet, because we have to say how we transport the ordinal structure. At first sight we should be able to simply apply univalence. However, this is not possible because the types $X : \mathcal{U}$ and $\operatorname{Ordinal}\,\mathcal{U} :\mathcal{U}^+$ live in different universes. The problem is that only elements of the same type can be compared for equality.

1. In the cumulative universe hierarchy of the HoTT book, we automatically have that $X : \mathcal{U}^+$ and hence, being equivalent to the type $\operatorname{Ordinal}\,\mathcal{U} : \mathcal{U}^+$, the type $X$ is equal to the type $\operatorname{Ordinal}\,\mathcal{U}$ by univalence. But this equality is an element of an identity type of the universe $\mathcal{U}^+$. Therefore when we transport the ordinal structure on the type $\operatorname{Ordinal}\,\mathcal{U}$ to the type $X$ along this equality and equip $X$ with it, we get an ordinal in the successor universe $\mathcal{U}^+$. But, in order to get the desired contradiction, we need to get an ordinal in $\mathcal{U}$.

2. In the non-cumulative universe hierarchy we adopt here, we face essentially the same difficulty. We cannot assert that $X : \mathcal{U}^+$ but we can promote $X$ to an equivalent type in the universe $\mathcal{U}^+$, and from this point on we reach the same obstacle as in the cumulative case.

So we have to transfer the ordinal structure from $\operatorname{Ordinal}\,\mathcal{U}$ to $X$ manually along the given equivalence, call it $$f : X \to \operatorname{Ordinal}\,\mathcal{U}.$$ We define the order of $X$ from that of $\operatorname{Ordinal}\,\mathcal{U}$ by $$ x \prec y = f(x) \triangleleft f(y). $$ It is laborious but not hard to see that this order satisfies the required axioms for making $X$ into an ordinal, except that it has values in $\mathcal{U}^+$ rather than $\mathcal{U}$. But this problem is solved by instead using the resized-down relation $\triangleleft^-$ discussed above, which is equivalent to $\triangleleft$ by univalence. $\square$

There are more types and sets in $\mathcal{U}^+$ than in $\mathcal{U}$

By a universe embedding we mean a map $$f : \mathcal{U} \to \mathcal{V}$$ of universes such that, for all $X : \mathcal{U}$, $$f(X) \simeq X.$$ Of course, any two universe embeddings of $\mathcal{U}$ into $\mathcal{V}$ are equal, by univalence, so that there is at most one universe embedding between any two universes. Moreover, universe embeddings are automatically type embeddings (meaning that they have propositional fibers).

So the following says that the universe $\mathcal{U}^+$ is strictly larger than the universe $\mathcal{U}$:

Theorem. The universe embedding $\mathcal{U} \to \mathcal{U}^+$ doesn't have a section and therefore is not an equivalence.

Proof. A section would give a type in the universe $\mathcal{U}$ equivalent to the type of ordinals in $\mathcal{U}$, but we have seen that there is no such type. $\square$

(However, by Theorem 29 of Injective types in univalent mathematics, if propositional resizing holds then the universe embedding $\mathcal{U} \to \mathcal{U}^+$ is a section.)

The same argument of the above theorem shows that there are more sets in $\mathcal{U}^+$ than in $\mathcal{U}$, because the type of ordinals is a set. For a universe $\mathcal{U}$ define the type $$\operatorname{hSet}\,\mathcal{U} : \mathcal{U}^+$$ by $$ \operatorname{hSet}\,\mathcal{U} = \Sigma A : \mathcal{U} , \text{$A$ is a set}.$$ By an hSet embedding we mean a map $$f : \operatorname{hSet}\,\mathcal{U} → \operatorname{hSet}\,\mathcal{V}$$ such that the underlying type of $f(\mathbb{X})$ is equivalent to the underlying type of $\mathbb{X}$ for every $\mathbb{X} : \operatorname{hSet}\,\mathcal{U}$, that is, $$ \operatorname{pr_1} (f (\mathbb{X})) ≃ \operatorname{pr_1}(\mathbb{X}). $$ Again there is at most one hSet-embedding between any two universes, hSet-embeddings are type embeddings, and we have:

Theorem. The hSet-embedding $\operatorname{hSet}\,\mathcal{U} \to \operatorname{hSet}\,\mathcal{U}^+$ doesn't have a section and therefore is not an equivalence.

There are more magmas and monoids in $\mathcal{U}^+$ than in $\mathcal{U}$

This is because the type of ordinals is a monoid under addition with the ordinal zero as its neutral element, and hence also a magma. If the inclusion of the type of magmas (respectively monoids) of one universe into that of the next were an equivalence, then we would have a small copy of the type of ordinals.

Theorem. The canonical embeddings $\operatorname{Magma}\,\mathcal{U} → \operatorname{Magma}\,\mathcal{U}^+$ and $\operatorname{Monoid}\,\mathcal{U} → \operatorname{Monoid}\,\mathcal{U}^+$ don't have sections and hence are not equivalences.

There are more groups in $\mathcal{U}^+$ than in $\mathcal{U}$

This case is more interesting.

The axiom of choice is equivalent to the statement that any non-empty set can be given the structure of a group. So if we assumed the axiom of choice we would be done. But we are brave and work without assuming excluded middle, and hence without choice, so that our results hold in any $\infty$-topos.

It is also the case that the type of propositions can be given the structure of a group if and only if the principle of excluded middle holds. And the type of propositions is a retract of the type of ordinals, which makes it unlikely that the type of ordinals can be given the structure of a group without excluded middle.

So our strategy is to embed the type of ordinals into a group, and the free group does the job.

1. First we need to show that the inclusion of generators, or the universal map into the free group, is an embedding.

2. But having a large type $X$ embedded into a type $Y$ is not enough to conclude that $Y$ is also large. For example, if $P$ is a proposition then the unique map $P \to \mathbb{1}$ is an embedding, and the unit type $\mathbb{1}$ is small but $P$ may be large.

3. So more work is needed to show that the group freely generated by the type of ordinals is large. We say that a map is small if each of its fibers is small, and large otherwise. De Jong and Escardo showed that if a map $X \to Y$ is small and the type $Y$ is small, then so is the type $X$, and hence if $X$ is large then so is $Y$. Therefore our approach is to show that the universal map into the free group is small. To do this, we exploit the fact that the type of ordinals is locally small (its identity types are all equivalent to small types).

But we want to be as general as possible, and hence work with a spartan univalent type theory which doesn't include higher inductive types other than propositional truncation. We include the empty type, the unit type, natural numbers, list types (which can actually be constructed from the other type formers), coproduct types, $\Sigma$-types, $\Pi$-types, identity types and a sequence of universes. We also assume the univalence axiom (from which we automatically get functional and propositional extensionality) and the axiom of existence of propositional truncations.

1. We construct the free group as a quotient of a type of words following Mines, Richman and Ruitenburg. To prove that the universal map is an embedding, one first proves a Church-Rosser property for the equivalence relation on words. It is remarkable that this can be done without assuming that the set of generators has decidable equality.

2. Quotients can be constructed from propositional truncation. This construction increases the universe level by one, but eliminates into any universe.

3. To resize back the quotient used to construct the group freely generated by the type of ordinals to the original universe, we exploit the fact that the type of ordinals is locally small.

4. As above, we have to transfer manually group structures between equivalent types of different universes, because univalence can't be applied.

Putting the above together, and leaving many steps to the Agda code, we get the following in our spartan univalent type theory.

Theorem. For any large, locally small set, the free group is also large and locally small.

Corollary. In any successor universe $\mathcal{U}^+$ there is a group which is not isomorphic to any group in the universe $\mathcal{U}$.

Corollary. The canonical embedding $\operatorname{Group}\,\mathcal{U} → \operatorname{Group}\,\mathcal{U}^+$ doesn't have a section and hence is not an equivalence.

Can we formulate and prove a general theorem of this kind that specializes to a wide variety of mathematical structures that occur in practice?

Tarides is very glad to announce our partnership with Ada Tech School.

Founded in 2019 and based in Paris (France), Ada Tech School, named for pioneer computer scientist Ada Lovelace, is a programming school designed for women but open to all. The program is driven by three values: feminism, empathy and singularity. Its mission is to facilitate access to programming positions and promote the feminization of tech, by creating training that tackles the gender and cultural biases of IT.

Unfortunate…

Tarides is very glad to announce our partnership with Ada Tech School.

Founded in 2019 and based in Paris (France), Ada Tech School, named for pioneer computer scientist Ada Lovelace, is a programming school designed for women but open to all. The program is driven by three values: feminism, empathy and singularity. Its mission is to facilitate access to programming positions and promote the feminization of tech, by creating training that tackles the gender and cultural biases of IT.

Unfortunately, the diversity of the candidate pool is very limited when a company tries to fill positions. Barely 10% of computer science students in France are girls. Ada Tech School is an excellent initiative to democratize software education amongst women. The school was created so that women can land a job easily in the IT industry through rigorous training, and then offer ongoing coaching and support to ascend the professional ladder within tech companies.

At Tarides, we believe that a healthy team is a diverse one; and that trust, fairness and inclusion are values needed to build a strong company.

We are committed to doing better, not only by hiring a diverse team and providing a welcoming work environment, but also by putting people first at every stage. This means providing fair and equitable compensation as well as meaningful career advancement opportunities for every employee.

We believe that a great technology always derives from great people, regardless of their background. Head here to see our currently-open positions.

We are pleased to announce the minor release of opam 2.0.8.

This new version contains some backported fixes:

• Critical for fish users! Don’t add . to PATH. [#4078]
• Fix sandbox script for newer ccache versions. [#4079 and #4087]
• Fix sandbox crash when ~/.cache is a symlink. [#4068]
• User modifications to the sandbox script are no longer overwritten by opam init. [#4020 & #4092]
• macOS sandbox script always mounts /tmp read-write, regardless of TMPDIR [#3742, addressing ocaml/opam-reposi…

We are pleased to announce the minor release of opam 2.0.8.

This new version contains some backported fixes:

• Critical for fish users! Don’t add . to PATH. [#4078]
• Fix sandbox script for newer ccache versions. [#4079 and #4087]
• Fix sandbox crash when ~/.cache is a symlink. [#4068]
• User modifications to the sandbox script are no longer overwritten by opam init. [#4020 & #4092]
• macOS sandbox script always mounts /tmp read-write, regardless of TMPDIR [#3742, addressing ocaml/opam-repository#13339]
• pre- and post-session hooks can now print to the console [#4359]
• Switch-specific pre/post sessions hooks are now actually run [#4472]
• Standalone opam-installer now correctly builds from sources [#4173]
• Fix arch variable detection when using 32bit mode on ARM64 and i486 [#4462]

A more complete release note is available.

Note: To homogenise macOS name on system detection, we decided to keep macos, and convert darwin to macos in opam. For the moment, in order to avoid breaking jobs & CIs, we keep uploading darwin & macos binaries, but from the 2.1.0 release, only macos ones will be kept.

Installation instructions (unchanged):

1. From binaries: run sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) or download manually from the Github “Releases” page to your PATH. In this case, don’t forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script.
2. From source, using opam: opam update; opam install opam-devel (then copy the opam binary to your PATH as explained, and don’t forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script)
3. From source, manually: see the instructions in the README.

We hope you enjoy this new minor version, and remain open to bug reports and suggestions.

NOTE: this article is cross-posted on opam.ocaml.org and ocamlpro.com, and published in discuss.ocaml.org. Please head to the latter for the comments!

About OCamlPro:

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users’ Club). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: contact@ocamlpro.com.

We are pleased to announce the minor release of opam 2.0.8.

This new version contains some backported fixes:

• Critical for fish users! Don't add . to PATH. [#4078]
• Fix sandbox script for newer ccache versions. [#4079 and #4087]
• Fix sandbox crash when ~/.cache is a symlink. [#4068]
• User modifications to the sandbox script are no longer overwritten by opam init. [#4020 & #4092]
• macOS sandbox script always mounts /tmp read-write, regardless of TMPDIR [#3742, addressing ocaml/opam-repository#13339]

We are pleased to announce the minor release of opam 2.0.8.

This new version contains some backported fixes:

• Critical for fish users! Don't add . to PATH. [#4078]
• Fix sandbox script for newer ccache versions. [#4079 and #4087]
• Fix sandbox crash when ~/.cache is a symlink. [#4068]
• User modifications to the sandbox script are no longer overwritten by opam init. [#4020 & #4092]
• macOS sandbox script always mounts /tmp read-write, regardless of TMPDIR [#3742, addressing ocaml/opam-repository#13339]
• pre- and post-session hooks can now print to the console [#4359]
• Switch-specific pre/post sessions hooks are now actually run [#4472]
• Standalone opam-installer now correctly builds from sources [#4173]
• Fix arch variable detection when using 32bit mode on ARM64 and i486 [#4462]

A more complete release note is available.

Note: To homogenise macOS name on system detection, we decided to keep macos, and convert darwin to macos in opam. For the moment, in order to avoid breaking jobs & CIs, we keep uploading darwin & macos binaries, but from the 2.1.0 release, only macos ones will be kept.

1. From binaries: run

   sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

   or download manually from the Github "Releases" page to your PATH. In this case, don't forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script.

2. From source, using opam:

   opam update; opam install opam-devel

   (then copy the opam binary to your PATH as explained, and don't forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script)

3. From source, manually: see the instructions in the README.

We hope you enjoy this new minor version, and remain open to bug reports and suggestions.

NOTE: this article is cross-posted on opam.ocaml.org and ocamlpro.com, and published in discuss.ocaml.org. Please head to the latter for the comments!

Feedback on this post is welcomed on Discuss!

On behalf of the opam team, it gives me great pleasure to announce the third beta release of opam 2.1. Don’t worry, you didn’t miss beta3 - we had an issue with a configure script that caused beta2 to report as beta3 in some instances, so we skipped to beta4 to avoid any further confusion!

We encourage you to try out this new beta release: there are instructions for doing so in our wiki. The instructions include taking a backup of your ~/.opam …

Feedback on this post is welcomed on Discuss!

On behalf of the opam team, it gives me great pleasure to announce the third beta release of opam 2.1. Don’t worry, you didn’t miss beta3 - we had an issue with a configure script that caused beta2 to report as beta3 in some instances, so we skipped to beta4 to avoid any further confusion!

We encourage you to try out this new beta release: there are instructions for doing so in our wiki. The instructions include taking a backup of your ~/.opam root as part of the process, which can be restored in order to wind back. Please note that local switches which are written to by opam 2.1 are upgraded and will need to be rebuilt if you go back to opam 2.0. This can either be done by removing _opam and repeating whatever you use in your build process to create the switch, or you can use opam switch export switch.export to backup the switch to a file before installing new packages. Note that opam 2.1 shouldn’t upgrade a local switch unless you upgrade the base packages (i.e. the compiler).

What’s new in opam 2.1?

• Switch invariants
• Improved options configuration (see the new option and expanded var sub-commands)
• Integration of system dependencies (formerly the opam-depext plugin), increasing their reliability as it integrates the solving step
• Creation of lock files for reproducible installations (formerly the opam-lock plugin)
• CLI versioning, allowing cleaner deprecations for opam now and also improvements to semantics in future without breaking backwards-compatibility
• Performance improvements to opam-update, conflict messages, and many other areas
• New plugins: opam-compiler and opam-monorepo

Switch invariants

In opam 2.0, when a switch is created the packages selected are put into the “base” of the switch. These packages are not normally considered for upgrade, in order to ease pressure on opam’s solver. This was a much bigger concern early on in opam 2.0’s development, but is less of a problem with the default mccs solver.

However, it’s a problem for system compilers. opam would detect that your system compiler version had changed, but be unable to upgrade the ocaml-system package unless you went through a slightly convoluted process with --unlock-base.

In opam 2.1, base packages have been replaced by switch invariants. The switch invariant is a package formula which must be satisfied on every upgrade and install. All existing switches’ base packages could just be expressed as package1 & package2 & package3 etc. but opam 2.1 recognises many existing patterns and simplifies them, so in most cases the invariant will be "ocaml-base-compiler" {= 4.11.1}, etc. This means that opam switch create my_switch ocaml-system now creates a switch invariant of "ocaml-system" rather than a specific version of the ocaml-system package. If your system OCaml package is updated, opam upgrade will seamlessly switch to the new package.

This also allows you to have switches which automatically install new point releases of OCaml. For example:

opam switch create ocaml-4.11 --formula='"ocaml-base-compiler" {>= "4.11.0" & < "4.12.0~"}' --repos=old=git+https://github.com/ocaml/opam-repository#a11299d81591
opam install utop

Creates a switch with OCaml 4.11.0 (the --repos= was just to select a version of opam-repository from before 4.11.1 was released). Now issue:

opam repo set-url old git+https://github.com/ocaml/opam-repository
opam upgrade

and opam 2.1 will automatically offer to upgrade OCaml 4.11.1 along with a rebuild of the switch. There’s not yet a clean CLI for specifying the formula, but we intend to iterate further on this with future opam releases so that there is an easier way of saying “install OCaml 4.11.x”.

opam depext integration

opam has long included the ability to install system dependencies automatically via the depext plugin. This plugin has been promoted to a native feature of opam 2.1.0 onwards, giving the following benefits:

• You no longer have to remember to run opam depext, opam always checks depexts (there are options to disable this or automate it for CI use). Installation of an opam package in a CI system is now as easy as opam install ., without having to do the dance of opam pin add -n/depext/install. Just one command now for the common case!
• The solver is only called once, which both saves time and also stabilises the behaviour of opam in cases where the solver result is not stable. It was possible to get one package solution for the opam depext stage and a different solution for the opam install stage, resulting in some depexts missing.
• opam now has full knowledge of depexts, which means that packages can be automatically selected based on whether a system package is already installed. For example, if you have neither MariaDB nor MySQL dev libraries installed, opam install mysql will offer to install conf-mysql and mysql, but if you have the MariaDB dev libraries installed, opam will offer to install conf-mariadb and mysql.

opam lock files and reproducibility

When opam was first released, it had the mission of gathering together scattered OCaml source code to build a community repository. As time marches on, the size of the opam repository has grown tremendously, to over 3000 unique packages with over 18000 unique versions. opam looks at all these packages and is designed to solve for the best constraints for a given package, so that your project can keep up with releases of your dependencies.

While this works well for libraries, we need a different strategy for projects that need to test and ship using a fixed set of dependencies. To satisfy this use-case, opam 2.0.0 shipped with support for using project.opam.locked files. These are normal opam files but with exact versions of dependencies. The lock file can be used as simply as opam install . --locked to have a reproducible package installation.

With opam 2.1.0, the creation of lock files is also now integrated into the client:

• opam lock will create a .locked file for your current switch and project, that you can check into the repository.
• opam switch create . --locked can be used by users to reproduce your dependencies in a fresh switch.

This lets a project simultaneously keep up with the latest dependencies (without lock files) while providing a stricter set for projects that need it (with lock files).

CLI Versioning

A new --cli switch was added to the first beta release, but it’s only now that it’s being widely used. opam is a complex enough system that sometimes bug fixes need to change the semantics of some commands. For example:

• opam show --file needed to change behaviour
• The addition of new controls for setting global variables means that the opam config was becoming cluttered and some things want to move to opam var
• opam switch create 4.11.1 still works in opam 2.0, but it’s really an OPAM 1.2.2 syntax.

Changing the CLI is exceptionally painful since it can break scripts and tools which themselves need to drive opam. CLI versioning is our attempt to solve this. The feature is inspired by the (lang dune ...) stanza in dune-project files which has allowed the Dune project to rename variables and alter semantics without requiring every single package using Dune to upgrade their dune files on each release.

Now you can specify which version of opam you expected the command to be run against. In day-to-day use of opam at the terminal, you wouldn’t specify it, and you’ll get the latest version of the CLI. For example: opam var --global is the same as opam var --cli=2.1 --global. However, if you issue opam var --cli=2.0 --global, you will told that --global was added in 2.1 and so is not available to you. You can see similar things with the renaming of opam upgrade --unlock-base to opam upgrade --update-invariant.

The intention is that --cli should be used in scripts, user guides (e.g. blog posts), and in software which calls opam. The only decision you have to take is the oldest version of opam which you need to support. If your script is using a new opam 2.1 feature (for example opam switch create --formula=) then you simply don’t support opam 2.0. If you need to support opam 2.0, then you can’t use --formula and should use --packages instead. opam 2.0 does not have the --cli option, so for opam 2.0 instead of --cli=2.0 you should set the environment variable OPAMCLI to 2.0. As with all opam command line switches, OPAMCLI is simply the equivalent of --cli which opam 2.1 will pick-up but opam 2.0 will quietly ignore (and, as with other options, the command line takes precedence over the environment).

Note that opam 2.1 sets OPAMCLI=2.0 when building packages, so on the rare instances where you need to use the opam command in a package build: command (or in your build system), you must specify --cli=2.1 if you’re using new features.

There’s even more detail on this feature in our wiki. We’re still finalising some details on exactly how opam behaves when --cli is not given, but we’re hoping that this feature will make it much easier in future releases for opam to make required changes and improvements to the CLI without breaking existing set-ups and tools.

What’s new since the last beta?

• opam now uses CLI versioning (#4385)
• opam now exits with code 31 if all failures were during fetch operations (#4214)
• opam install now has a --download-only flag (#4036), allowing opam’s caches to be primed
• opam init now advises the correct shell-specific command for eval $(opam env) (#4427)
• post-install hooks are now allowed to modify or remove installed files (#4388)
• New package variable opamfile-loc with the location of the installed package opam file (#4402)
• opam update now has --depexts flag (#4355), allowing the system package manager to update too
• depext support NetBSD and DragonFlyBSD added (#4396)
• The format-preserving opam file printer has been overhauled (#3993, #4298 and #4302)
• pins are now fetched in parallel (#4315)
• os-family=ubuntu is now treated as os-family=debian (#4441)
• opam lint now checks that strings in filtered package formulae are booleans or variables (#4439)

and many other bug fixes as listed on the release page.

New Plugins

Several features that were formerly plugins have been integrated into opam 2.1.0. We have also developed some new plugins that satisfy emerging workflows from the community and the core OCaml team. They are available for use with the opam 2.1 beta as well, and feedback on them should be directed to the respective GitHub trackers for those plugins.

opam compiler

The opam compiler plugin can be used to create switches from various sources such as the main opam repository, the ocaml-multicore fork, or a local development directory. It can use Git tag names, branch names, or PR numbers to specify what to install.

Once installed, these are normal opam switches, and one can install packages in them. To iterate on a compiler feature and try opam packages at the same time, it supports two ways to reinstall the compiler: either a safe and slow technique that will reinstall all packages, or a quick way that will just overwrite the compiler in place.

opam monorepo

The opam monorepo plugin lets you assemble standalone dune workspaces with your projects and all of their opam dependencies, letting you build it all from scratch using only Dune and OCaml. This satisfies the “monorepo” workflow which is commonly requested by large projects that need all of their dependencies in one place. It is also being used by projects that need global cross-compilation for all aspects of a codebase (including C stubs in packages), such as the MirageOS unikernel framework.

Next Steps

This is anticipated to be the final beta in the 2.1 series, and we will be moving to release candidate status after this. We could really use your help with testing this release in your infrastructure and projects and let us know if you run into any blockers. If you have feature requests, please also report them on our issue tracker -- we will be planning the next release cycle once we ship opam 2.1.0 shortly.

It is my pleasure to have the opportunity to speak at the University of Wisconsin Logic seminar. The hosts are graciously keeping the seminar open for everyone. I will speak about a favorite topic of mine:

Synthetic mathematics with an excursion into computability theory

Speaker: Andrej Bauer (University of Ljubljana)
Location: University of Wisconsin Logic seminar
Time: February 8th 2021, 21:30 UTC (3:30pm CST in Wisconsin, 22:30 CET in Ljubljana)
Video link: the Zoom link is available at the…

It is my pleasure to have the opportunity to speak at the University of Wisconsin Logic seminar. The hosts are graciously keeping the seminar open for everyone. I will speak about a favorite topic of mine:

Synthetic mathematics with an excursion into computability theory

Speaker: Andrej Bauer (University of Ljubljana)
Location: University of Wisconsin Logic seminar
Time: February 8th 2021, 21:30 UTC (3:30pm CST in Wisconsin, 22:30 CET in Ljubljana)
Video link: the Zoom link is available at the seminar page

Abstract:

According to Felix Klein, “synthetic geometry is that which studies figures as such, without recourse to formulae, whereas analytic geometry consistently makes use of such formulae as can be written down after the adoption of an appropriate system of coordinates”. To put it less eloquently, the synthetic method axiomatizes geometry directly by construing points and lines as primitive notions, whereas the analytic method builds a model, the Euclidean plane, from the real numbers.

Do other branches of mathematics posses the synthetic method, too? For instance, what would “synthetic topology” look like? To build spaces out of sets, as topologists usually do, is the analytic way. The synthetic approach must construe spaces as primitive and axiomatize them directly, without any recourse to sets. It cannot introduce continuity as a desirable property of functions, for that would be like identifying straight lines as the non-bending curves.

It is indeed possible to build the synthetic worlds of topology, smooth analysis, measure theory, and computability. In each of them, the basic structure – topological, smooth, measurable, computable – is implicit by virtue of permeating everything, even logic itself. The synthetic worlds demand an economy of thought that the unaccustomed mind finds frustrating at first, but eventually rewards it with new elegance and conceptual clarity. The synthetic method is still fruitfully related to the analytic method by interpretation of the former in models provided by the latter.

We demonstrate the approach by taking a closer look at synthetic computability, whose central axiom states that there are countably many countable subsets of the natural numbers. The axiom is validated and explained by its interpretation in the effective topos, where it corresponds to the familiar fact that the computably enumerable sets may be computably enumerated. Classic theorems of computability may be proved in a straightforward manner, without reference to any notion of computation. We end by showing that in synthetic computability Turing reducibility is expressed in terms of sequential continuity of maps between directed-complete partial orders.

The slides and the video recording of the talk are now available.

OCamlPro was created in 2011 to advocate the adoption of the OCaml language and formal methods in general in the industry. While building a team of highly-skilled engineers, we navigated through our expertise domains, delivering works on the OCaml language and tooling, training companies to the use of strongly-typed languages like OCaml but also Rust, tackling formal verification challenges with formal methods, maintaining the SMT solver Alt-Ergo, designing languages and tools for smart contrac…

OCamlPro was created in 2011 to advocate the adoption of the OCaml language and formal methods in general in the industry. While building a team of highly-skilled engineers, we navigated through our expertise domains, delivering works on the OCaml language and tooling, training companies to the use of strongly-typed languages like OCaml but also Rust, tackling formal verification challenges with formal methods, maintaining the SMT solver Alt-Ergo, designing languages and tools for smart contracts and blockchains, and more!

In this article, as every year, we review some of the work we did during 2020, in many different worlds.

Table of contents

• In the World of OCaml
  • Flambda & Compilation Team
  • Opam, the OCaml Package Manager
  • Encouraging OCaml Adoption: Trainings and Resources for OCaml
  • Open Source Tooling and Libraries for OCaml
  • Supporting the OCaml Software Foundation
  • Events
• In the World of Formal Methods
  • Alt-Ergo Development
  • Alt-Ergo Users’ Club and R&D Projects
  • Alt-Ergo’s Roadmap
• In the World of Rust
• In the World of Blockchain Languages

We warmly thank all our partners, clients and friends for their support and collaboration during this peculiar year!

The first lockdown was a surprise and we took advantage of this special moment to go over our past contributions and sum it up in a timeline that gives an overview of the key events that made OCamlPro over the years. The timeline format is amazing to reconnect with our history and to take stock in our accomplishments.

Now this will turn into a generic timeline edition tool on the Web, stay tuned if you are interested in our internal project to be available to the general public! If you think that a timeline would fit your needs and audience, we designed a simplistic tool, tailored for users who want complete control over their data.

In the World of OCaml

Flambda & Compilation Team

* Work by Pierre Chambart, Vincent Laviron, Guillaume Bury, Pierrick Couderc and Louis Gesbert

OCamlPro is proud to be working on Flambda2, an ambitious work on an OCaml optimizing compiler, in close collaboration with Mark Shinwell from our long-term partner and client Jane Street. Flambda focuses on reducing the runtime cost of abstractions and removing as many short-lived allocations as possible. In 2020, the Flambda team worked on a considerable number of fixes and improvements, transforming Flambda2 from an experimental prototype to a version ready for testing in production!

This year also marked the conclusion of our work on the pack rehabilitation (see our two recent posts Part1 and Part2, and a much simpler Version in 2011). Our work aimed to give them a new youth and utility by adding the possibility to generate functors or recursive packs. This improvement allows programmers to define big functors, functors that are split among multiple files, resulting in what we can view as a way to implement some form of parameterized libraries.

This work is allowed thanks to Jane Street’s funding.

Opam, the Ocaml Package Manager

* Work by Raja Boujbel, Louis Gesbert and Thomas Blanc

Opam is OCamlPro’s source-based package manager. The first specification draft was written in early 2012 and went on to become OCaml’s official package manager — though it may be used for other languages and projects, since Opam is language-agnostic! If you need to install, upgrade and manage your compiler(s), tools and libraries easily, Opam is meant for you. It supports multiple simultaneous compiler installations, flexible package constraints, and a Git-friendly development workflow. 

Our 2020 work on Opam led to the release of two versions of opam 2.0 with small fixes, and the release of three alphas and two betas of Opam 2.1! 

Opam 2.1.0 will soon go to release candidate and will introduce a seamless integration of depexts (system dependencies handling), dependency locking, pinning sub-directories, invariant-based definition for Opam switches, the configuration of Opam from the command-line without the need for a manual edition of the configuration files, and the CLI versioning for better handling of CLI evolutions.

This work is greatly helped by Jane Street’s funding and support.

Encouraging Ocaml Adoption: Trainings and Resources for Ocaml

* Work by Pierre Chambart, Vincent Laviron, Adrien Champion, Mattias, Louis Gesbert and Thomas Blanc

OCamlPro is also a training centre. We organise yearly training sessions for programmers from multiple companies in our offices: from OCaml to OCaml tooling to Rust! We can also design custom and on-site trainings to meet specific needs.

We released a brand new version of TryOCaml, a tool born from our work on Learn-OCaml! Try OCaml has been highly praised by professors at the beginning of the Covid lockdown. Even if it can be used as a personal sandbox, it’s also possible to adapt its usage for classes. TryOCaml is a hassle-free tool that lowers significantly the barriers to start coding in OCaml, as no installation is required.

We regularly release cheat sheets for developers: in 2020, we shared the long-awaited Opam 2.0 cheat sheet, with a new theme! In just two pages, you’ll have in one place the everyday commands you need as an Opam user. We also shine some light on unsung features which may just change your coding life. 

2020 was also an important year for the OCaml language itself: we were pleased to welcome OCaml 4.10! One of the highlights of the release was the “Best-fit” Garbage Collector Strategy. We had an in-depth look at this exciting change.

This work is self-funded by OCamlPro as part of its effort to ease the adoption of OCaml.

Open Source Tooling and Libraries for OCaml

* Work by Fabrice Le Fessant, Léo Andrès and David Declerck

OCamlPro has a long history of developing open source tooling and libraries for the community. 2020 was no exception!

drom is a simple tool to create new OCaml projects that will use best OCaml practices, i.e. Opam, Dune and tests. Its goal is to provide a cargo-like user experience and helps onboarding new developers in the community. drom is available in the official opam repository.

directories is a new OCaml Library that provides configuration, cache and data paths (and more!). The library follows the suitable conventions on Linux, MacOS and Windows.

opam-bin is a framework to create and use binary packages with Opam. It enables you to create, use and share binary packages easily with opam, and to create as many local switches as you want spending no time, no disk space! If you often use Opam, opam-bin is a must-have!

We also released a number of libraries, focused on making things easy for developers… so we named them with an ez_ prefix: ez_cmdliner provides an Arg-like interface for cmdliner, ez_file provides simple functions to read and write files, ez_subst provides easily configurable string substitutions for shell-like variable syntax, ez_config provides abstract options stored in configuration files with an OCaml syntax. There are also a lot of ezjs-* libraries, that are bindings to Javascript libraries that we used in some of our js_of_ocaml projects.

This work was self-funded by OCamlPro as part of its effort to improve the OCaml ecosystem.

Supporting the OCaml Software Foundation

OCamlPro was proud and happy to initiate the OCaml User Survey 2020 as part of the mission of the OCaml Software Foundation. The goal of the survey was to better understand the community and its needs. The final results have not yet been published by the Foundation, we are looking forward to reading them soon!

Events

Though the year took its toll on our usual tour of the world conferences and events, OCamlPro members still took part in the annual 72-hour team programming competition organised by the International Conference on Functional Programming (ICFP). Our joint team “crapo on acid” went through the final!

In the World of Formal Methods

* Work by Albin Coquereau, Mattias, Sylvain Conchon, Guillaume Bury and Louis Rustenholz

Sylvain Conchon joined us as Formal Methods Chief Scientific Officer in 2020!

Alt-Ergo Development

OCamlPro develops and maintains Alt-Ergo, an automatic solver of mathematical formulas designed for program verification and based on Satisfiability Modulo Theories (SMT). Alt-Ergo was initially created within the VALS team at University of Paris-Saclay.

In 2020, we focused on the maintainability of our solver. The first part of this work was to maintain and fix issues within the already released version. The 2.3.0 (released in 2019) had some issues that needed to be fixed (minor releases).

The second part of the maintainability of Alt-Ergo contains more major features. All these features were released in the new version 2.4.0 of Alt-Ergo. The main goal of this release was to focus on the user experience and the documentation. This release also contains bug fixes and many other improvements. Alt-Ergo has a new documentation and in particular a documentation on its native syntax.

We also tried to improve the command line experience of our tools with the use of the cmdliner library to parse Alt-Ergo option. This library allows us to improve the manpage of our tool. We tried to harmonise the debug messages and to improve all of Alt-Ergo’s outputs to make it clearer for the users.

Alt-Ergo Users’ Club and R&D Projects

We thank our partners from the Alt-Ergo Users’ Club, Adacore, CEA List, MERCE (Mitsubishi Electric R&D Centre Europe) and Trust-In-Soft, for their trust. Their support allows us to maintain our tool.

The club was launched in 2019 and the second annual meeting of the Alt-Ergo Users’ Club was held in mid-February 2020. Our annual meeting is the perfect place to review each partner’s needs regarding Alt-Ergo. This year, we had the pleasure of receiving our partners to discuss the roadmap for future Alt-Ergo developments and enhancements. If you want to join us for the next meeting (coming soon), contact us!

We also want to thank our partners from the FUI R&D Project LCHIP. Thanks to this project, we were able to add a new major feature in Alt-Ergo: the support for incremental commands (push, pop and check-sat-assuming) from the smt-lib2 standard.

Alt-Ergo’s Roadmap

Some of the work we did in 2020 is not yet available. Thanks to our partner MERCE (Mitsubishi Electric R&D Centre Europe), we worked on the SMT model generation. Alt-Ergo is now (partially) able to output a model in the smt-lib2 format. Thanks to the Why3 team from University of Paris-Saclay, we hope that this work will be available in the Why3 platform to help users in their program verification efforts.

Another project was launched in 2020 but is still in early development: the complete rework of our Try-Alt-Ergo website with new features such as model generation. Try Alt-Ergo (current version) allows users to use Alt-Ergo directly from their browsers (Firefox, Chromium) without the need of a server for computations.

This work needed a JavaScript compatible version of Alt-Ergo. We have made some work to build our solver in two versions, one compatible with Node.js and another as a webworker. We hope that this work can make it easier to use our SMT solver in web applications.

This work is funded in part by the FUI R&D Project LCHIP, MERCE, Adacore and with the support of the Alt-Ergo Users’ Club.

In the World of Rust

* Work by Adrien Champion

As OCaml-ians, we naturally saw in the Rust language a beautiful complement to our approach. One opportunity to explore this state-of-the art language has been to pursue our work on ocp-memprof and build Memthol, a visualizer and analyzer to profile OCaml programs. It works on memory dumps containing information about the size and (de)allocation date of part of the allocations performed by some execution of a program.

Between lockdowns, we’ve also been able to hold our Rust training. It’s designed as a highly-modular vocational course, from 1 to 4 days. The training covers a beginner introduction to Rust’s basics features, crucial features and libraries for real-life development and advanced features, all through complex use-cases one would find in real life. 

This work was self-funded by OCamlPro as part of our exploration of other statically and strongly typed functional languages.

In the World of Blockchain Languages

* Work by David Declerck and Steven de Oliveira

One of our favourite activities is to develop new programming languages, specialized for specific domains, but with nice properties like clear semantics, strong typing, static typing and functional features. In 2020, we applied our skills in the domain of blockchains and smart contracts, with the creation of a new language, Love, and work on a well-known language, Solidity.

In 2020, our blockchain experts released Love, a type-safe language with a ML syntax and suited for formal verification. In a few words, Love is designed to be expressive for fast development, efficient in execution time and cheap in storage, and readable in terms of smart contracts auditability. Yet, it has a clear and formal semantics and a strong type system to detect bugs. It allows contracts to use other contracts as libraries, and to call viewers on other contracts. Contracts developed in Love can also be formally verified.

We also released a Solidity parser and printer written in OCaml using Menhir, and used it to implement a full interpreter directly in a blockchain. Solidity is probably the most used language for smart contracts, it was first born on Ethereum but many other blockchains provide it as a way to easily onboard new developers coming from the Ethereum ecosystem. In the future, we plan to extend this work with formal verification of Solidity smart contracts.

This is a joint effort with Origin Labs, the company created to tackle blockchain-related challenges.

Towards 2021

Adaptability and continuous improvement, that’s what 2020 brought to OCamlPro! We will remember 2020 as a complicated year, but one that allowed us to surpass ourselves and challenge our projects. We are very proud of our team who all continued to grow, learn, and develop our projects in this particular context. We are more motivated than ever for the coming year, which marks our tenth year anniversary! We’re excited to continue sharing our knowledge of the OCaml world and to accompany you in your own projects. 

Drop us a line or call us if you’d like to collaborate with us, we’d love to hear from you!

Merlin is a language server for the OCaml programming language; that is, a daemon that connects to your favourite text editor and provides the usual services of an IDE: instant feedback on warnings and errors, autocompletion, "type of the code under the cursor", "go to definition", etc. As we (Frédéric Bour, Ulysse Gérard and I) are about to do a new major release, we thought now would be a good time to talk a bit about some of the changes that are going into this release.

Project configurati…

Merlin is a language server for the OCaml programming language; that is, a daemon that connects to your favourite text editor and provides the usual services of an IDE: instant feedback on warnings and errors, autocompletion, "type of the code under the cursor", "go to definition", etc. As we (Frédéric Bour, Ulysse Gérard and I) are about to do a new major release, we thought now would be a good time to talk a bit about some of the changes that are going into this release.

Project configuration

Since its very first release, merlin has been getting information about the project being worked on through a .merlin file, which used to be written by the user, but is now often generated by build systems.

This had the advantage of being fairly simple: Merlin would just look in the current directory if such a file existed, otherwise it would look in the parent directories until it found one; and then read it. But there were also some sore points: the granularity of the configuration is the directory not the file, and this information is duplicated from the build system configuration (be it dune, Makefiles, or, back in the days, ocamlbuild).

After years of thinking about it, we've finally decided to make some light changes to this process. Since version 3.4, when it scans the filesystem Merlin is now looking for either a .merlin file or a dune (or dune-project) file. And when it finds one of those, it starts an external process in the directory where that file lives, and asks that process for the configuration of the ml(i) file being edited.

The process in charge of communicating the configuration to Merlin will either be a specific dune subcommand (when a dune file is found), or a dedicated .merlin reader program.

We see several advantages in doing things this way (rather than, for instance, changing the format of .merlin files):

1. this change is entirely backward compatible, and indeed the transition has already happened silently; although dune is still emitting .merlin files, this will only stop with dune 2.8.
2. externalizing the reading of .merlin files and simply requiring a "normalized" version of the config (i.e. with no mention of packages, just of flags and paths) allowed us to simplify the internals of Merlin.
3. talking to the build system directly not only gets us a much finer grained configuration (which is important when you build different executables with different flags in the same directory, or if you apply different ppxes to different files of a library), it opens the door to getting a nicer behavior of Merlin in some circumstances. For instance, the build system can (and does) tell Merlin when the project isn't built. Currently we only report that information to the user when he asks for errors, alongside all the other (mostly rubbish) errors. Which is already helpful in itself. But in the future we can start filtering the other errors to only report those that would remain even after building the project (e.g. parse errors).

There are however some changes to look out for:

• people who still use .merlin files but do not install Merlin using opam need to make sure to also have the dot-merlin-reader binary in their PATH (it is available as an opam package, but is also buildable from Merlin's git repository)
• vim and emacs users who could previously load packages interactively (by calling M-x merlin-use or :MerlinUse) cannot do that anymore, since Merlin itself stopped linking with findlib. They'll have to write a .merlin file.

Dropping support for old versions of OCaml

Until now, every release of Merlin has kept support from OCaml 4.02 to the latest version of OCaml available at the time of that release.

We have done this by having one version of "the frontend" (i.e. handling of buffer state, project configuration; analyses like jump-to-definition, prefix-completion, etc.), but several versions of "the backend" (OCaml's ASTs, parser and typechecker), and choosing at build time which one to use. The reason for doing this instead of having, for instance, one branch of Merlin per version of OCaml, is that while the backends are fairly stable once released, Merlin's frontend keeps evolving. Having just one version of it makes it easier to add features and fix bugs (patches don't need to be duplicated), whilst ensuring that Merlin's behavior is consistent across every version of OCaml that we support.

For this to work however, one needs a well defined API between the frontend and all the versions of the backend. This implies mapping every versions of OCaml's internal ASTs (which receive modifications from one version to the next), to a unified one, so as to keep Merlin's various features version agnostic. But it also means being resilient to OCaml's internal API changes. For instance between 4.02 and 4.11 there were big refactorings impacting: the way one accesses the typing environment, the way one accesses the "load path" (the part of the file system the compiler/Merlin is aware of), the way error message are produced, ...

The rate of changes on the compiler is a lot higher than what it was when we first started Merlin (7 years ago now!) which doesn't just mean that we have to spend more and more time on updating the common interface, but also that the interface is getting harder to define. Recently (with the 4.11 release) some of the changes were significant enough that for some parts of the backend we just didn't manage to produce a single interface to access old and new versions, so instead we had to start duplicating and specializing parts of the frontend. And we don't expect things to get much better in the near future.

Furthermore, Merlin's backends are patched to be more resilient to parsing and typing errors in the user's code. Those patches also need to be evolved at each new release of the compiler. The work required to keep the "unified interface" working was taking time away from updating our patches properly, and our support of user errors has slowly been getting worse over the past few years, resulting in less precise type information when asked, incomplete results when asking for auto-completion, etc.

Therefore we have decided to stop dragging older versions of OCaml along. We plan to switch to a system where we have one branch of Merlin per version of OCaml, and each opam release of Merlin will only be buildable with one version of OCaml. We will keep maintaining all the relatively recent branches (that is: 4.02 definitely will not get fixes, but 4.06 is still in the clear). However, all the new features will be developed against the latest version of OCaml and cherry-picked to older branches if, and only if, there are no merge conflicts and they work as expected without changes.

We hope that this will make it easier for us to update to new versions of OCaml (actually, we already know it does, working on adding support for 4.12 was easier than for any of the other recent versions), will allow us to clean up Merlin's codebase (let's call that a work in progress), and will free some time to work on new features.

You might wonder what all this changes for you, as a user, in practice. Well, it depends:

• if you install Merlin from opam: nothing, or almost nothing. Everything that you currently do with Merlin will keep working. In the future, perhaps some new feature will appear that won't work on all versions. But that day hasn't come yet.
• if you install Merlin some other way (manually?): you can't just fetch master and build it anymore. You have to pick the appropriate branch for your version of OCaml.
• if you're reusing Merlin's codebase as part of another project and (even worse) have patches on it: come and talk to us if you haven't done so already! We can try and integrate your patches, so that you only need to worry about vendoring the right version(s) for your needs.

Over the years, Merlin has received bugfixes and improvements from a long list of people, but for the upcoming release Frédéric and I are particularly grateful to Rudi Grinberg, a long time and regular contributor who also maintains the OCaml LSP project, as well as Ulysse Gérard, who joined our team a year ago now. They are in particular the main authors of the work to improve the handling of projects' configuration.

We hope you'll be as excited as us by all these changes!

Introduction

2020 was an intense year. I hope you're healthy and keep being healthy. I am privileged (as lots of software engineers and academics are) to be able to work from home during the pandemic. Let's not forget people in less privileged situations, and let’s try to give them as much practical, psychological and financial support as we can these days. And as much joy as possible to everyone around :)

I cancelled the autumn MirageOS retreat due to the pandemic. Instead I collected donati…

Introduction

2020 was an intense year. I hope you're healthy and keep being healthy. I am privileged (as lots of software engineers and academics are) to be able to work from home during the pandemic. Let's not forget people in less privileged situations, and let’s try to give them as much practical, psychological and financial support as we can these days. And as much joy as possible to everyone around :)

I cancelled the autumn MirageOS retreat due to the pandemic. Instead I collected donations for our hosts in Marrakech - they were very happy to receive our financial support, since they had a difficult year, since their income is based on tourism. I hope that in autumn 2021 we'll have an on-site retreat again.

For 2021, we (at robur) got a grant from the EU (via NGI pointer) for "Deploying MirageOS" (more details below), and another grant from OCaml software foundation for securing the opam supply chain (using conex). Some long-awaited releases for MirageOS libraries, namely a ssh implementation and a rewrite of our git implementation have already been published.

With my MirageOS view, 2020 was a pretty successful year, where we managed to add more features, fixed lots of bugs, and paved the road ahead. I want to thank OCamlLabs for funding work on MirageOS maintenance.

Recap 2020

Here is a very subjective random collection of accomplishments in 2020, where I was involved with some degree.

NetHSM

NetHSM is a hardware security module in software. It is a product that uses MirageOS for security, and is based on the muen separation kernel. We at robur were heavily involved in this product. It already has been security audited by an external team. You can pre-order it from Nitrokey.

TLS 1.3

Dating back to 2016, at the TRON (TLS 1.3 Ready or NOt), we developed a first draft of a 1.3 implementation of OCaml-TLS. Finally in May 2020 we got our act together, including ECC (ECDH P256 from fiat, X25519 from hacl) and testing with tlsfuzzer, and release tls 0.12.0 with TLS 1.3 support. Later we added ECC ciphersuites to TLS version 1.2, implemented ChaCha20/Poly1305, and fixed an interoperability issue with Go's implementation.

Mirage-crypto provides the underlying cryptographic primitives, initially released in March 2020 as a fork of nocrypto -- huge thanks to pqwy for his great work. Mirage-crypto detects CPU features at runtime (thanks to Julow) (bugfix for bswap), using constant time modular exponentation (powm_sec) and hardens against Lenstra's CRT attack, supports compilation on Windows (thanks to avsm), async entropy harvesting (thanks to seliopou), 32 bit support, chacha20/poly1305 (thanks to abeaumont), cross-compilation (thanks to EduardoRFS) and various bug fixes, even memory leak (thanks to talex5 for reporting several of these issues), and RSA interoperability (thanks to psafont for investigation and mattjbray for reporting). This library feels very mature now - being used by multiple stakeholders, and lots of issues have been fixed in 2020.

Qubes Firewall

The MirageOS based Qubes firewall is the most widely used MirageOS unikernel. And it got major updates: in May Steffi announced her and Mindy's work on improving it for Qubes 4.0 - including dynamic firewall rules via QubesDB. Thanks to prototypefund for sponsoring.

In October 2020, we released Mirage 3.9 with PVH virtualization mode (thanks to mato). There's still a memory leak to be investigated and fixed.

IPv6

In December, with Mirage 3.10 we got the IPv6 code up and running. Now MirageOS unikernels have a dual stack available, besides IPv4-only and IPv6-only network stacks. Thanks to nojb for the initial code and MagnusS.

Turns out this blog, but also robur services, are now available via IPv6 :)

Albatross

Also in December, I pushed an initial release of albatross, a unikernel orchestration system with remote access. Deploy your unikernel via a TLS handshake -- the unikernel image is embedded in the TLS client certificates.

Thanks to reynir for statistics support on Linux and improvements of the systemd service scripts. Also thanks to cfcs for the initial Linux port.

CA certs

For several years I postponed the problem of how to actually use the operating system trust anchors for OCaml-TLS connections. Thanks to emillon for initial code, there are now ca-certs and ca-certs-nss opam packages (see release announcement) which fills this gap.

Unikernels

I developed several useful unikernels in 2020, and also pushed a unikernel gallery to the Mirage website:

Traceroute in MirageOS

I already wrote about traceroute which traces the routing to a given remote host.

Unipi - static website hosting

Unipi is a static site webserver which retrieves the content from a remote git repository. Let's encrypt certificate provisioning and dynamic updates via a webhook to be executed for every push.

TLSTunnel - TLS demultiplexing

The physical machine this blog and other robur infrastructure runs on has been relocated from Sweden to Germany mid-December. Thanks to UPS! Fewer IPv4 addresses are available in the new data center, which motivated me to develop tlstunnel.

The new behaviour is as follows (see the monitoring branch):

• listener on TCP port 80 which replies with a permanent redirect to https
• listener on TCP port 443 which forwards to a backend host if the requested server name is configured
• its configuration is stored on a block device, and can be dynamically changed (with a custom protocol authenticated with a HMAC)
• it is setup to hold a wildcard TLS certificate and in DNS a wildcard entry is pointing to it
• setting up a new service is very straightforward: only the new name needs to be registered with tlstunnel together with the TCP backend, and everything will just work

2021

The year started with a release of awa, a SSH implementation in OCaml (thanks to haesbaert for initial code). This was followed by a git 3.0 release (thanks to dinosaure).

Deploying MirageOS - NGI Pointer

For 2021 we at robur received funding from the EU (via NGI pointer) for "Deploying MirageOS", which boils down into three parts:

• reproducible binary releases of MirageOS unikernels,
• monitoring (and other devops features: profiling) and integration into existing infrastructure,
• and further documentation and advertisement.

Of course this will all be available open source. Please get in touch via eMail (team aT robur dot coop) if you're eager to integrate MirageOS unikernels into your infrastructure.

We discovered at an initial meeting with an infrastructure provider that a DNS resolver is of interest - even more now that dnsmasq suffered from dnspooq. We are already working on an implementation of DNSSec.

MirageOS unikernels are binary reproducible, and infrastructure tools are available. We are working hard on a web interface (and REST API - think of it as "Docker Hub for MirageOS unikernels"), and more tooling to verify reproducibility.

Conex - securing the supply chain

Another funding from the OCSF is to continue development and deploy conex - to bring trust into opam-repository. This is a great combination with the reproducible build efforts, and will bring much more trust into retrieving OCaml packages and using MirageOS unikernels.

MirageOS 4.0

Mirage so far still uses ocamlbuild and ocamlfind for compiling the virtual machine binary. But the switch to dune is close, a lot of effort has been done. This will make the developer experience of MirageOS much more smooth, with a per-unikernel monorepo workflow where you can push your changes to the individual libraries.

Footer

If you want to support our work on MirageOS unikernels, please donate to robur. I'm interested in feedback, either via twitter, hannesm@mastodon.social or an issue on the data repository.

A new release of Alt-Ergo (version 2.4.0) is available.

You can get it from Alt-Ergo’s website. The associated opam package will be published in the next few days.

This release contains some major novelties:

• Alt-Ergo supports incremental commands (push/pop) from the smt-lib standard.
• We switched command line parsing to use cmdliner. You will need to use --<option name> instead of -<option name>. Some options have also been renamed, see the manpage or the documentati…

A new release of Alt-Ergo (version 2.4.0) is available.

You can get it from Alt-Ergo’s website. The associated opam package will be published in the next few days.

This release contains some major novelties:

• Alt-Ergo supports incremental commands (push/pop) from the smt-lib standard.
• We switched command line parsing to use cmdliner. You will need to use --<option name> instead of -<option name>. Some options have also been renamed, see the manpage or the documentation.
• We improved the online documentation of your solver, available here.

This release also contains some minor novelties:

• .mlw and .why extension are depreciated, the use of .ae extension is advised.
• Add --input (resp --output) option to manually set the input (resp output) file format
• Add --pretty-output option to add better debug formatting and to add colors
• Add exponentiation operation, ** in native Alt-Ergo syntax. The operator is fully interpreted when applied to constants
• Fix --steps-count and improve the way steps are counted (AdaCore contribution)
• Add --instantiation-heuristic option that can enable lighter or heavier instantiation
• Reduce the instantiation context (considered foralls / exists) in CDCL-Tableaux to better mimic the Tableaux-like SAT solver
• Multiple bugfixes

The full list of changes is available here. As usual, do not hesitate to report bugs, to ask questions, or to give your feedback!

About OCamlPro:
OCamlPro SAS is an INRIA spin-off company created in April 2011 to promote the use of the OCaml programming language in the industrial sector. It actively participates in research and development aimed at improving safety and security in the security of computer applications in general. You will find more information on our website: http://www.ocamlpro.com.

The Coq development team is proud to announce the immediate availability of Coq 8.13.0

Highlights:

• Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays.
• Introduction of definitional proof irrelevance for the equality type defined in the SProp sort.
• Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation availab…

The Coq development team is proud to announce the immediate availability of Coq 8.13.0

Highlights:

• Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays.
• Introduction of definitional proof irrelevance for the equality type defined in the SProp sort.
• Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation available to print an expression, which might introduce changes in printing behavior.

Please see the changelog to learn more about this release.

The Oxbridge Women in Computer Science conference is an annual one-day event hosted by the Universities of Oxford and Cambridge (UK). The conference is free and open to everyone from any discipline, regardless of gender identity. Its purpose is to spotlight the successes of women within computer science and strengthen the network of women in computer science within a supportive and friendly environment.

This year, the conference was organised by the University of Cambridge and was held virtually…

The Oxbridge Women in Computer Science conference is an annual one-day event hosted by the Universities of Oxford and Cambridge (UK). The conference is free and open to everyone from any discipline, regardless of gender identity. Its purpose is to spotlight the successes of women within computer science and strengthen the network of women in computer science within a supportive and friendly environment.

This year, the conference was organised by the University of Cambridge and was held virtually on December 7th.

Tarides is very glad to sponsor this event as we strongly believe that diversity and inclusive culture is a key factor in building a competitive and innovative company. Our employees come from 8 different countries and are 1⁄3 women. Tarides promotes transparency, openness and autonomy, creating a work atmosphere auspicious for employees to strive in their work, to solve novel, impactful and technical challenges. By working on open-source projects, a collaboration is possible with worldwide experts from both academia and industry, encouraging continuous training and education; in this context, it is very important to have teams with diverse backgrounds and experience.

The underrepresentation of women in tech, and particularly in computer science, is not a new problem and gender equality remains a major issue in the corporate world. By celebrating female computer scientists, as during the Oxbridge Women in Computer Science Conference, it will hopefully encourage more women to pursue their interests and careers in the tech field. Head here to see our currently-open positions.

For the event, we made a short video to experience a day in the life of a software engineer: