Between March 6th and March 13th 2019, I attended the Mirage retreat organized by Hannes Mehnert in Marrakesh, Morocco.

The Mirage retreat takes place in an artist residency organized as a hostel (shared rooms with simple beds). Hannes gathers a lot of people whose activity is relevant to the Mirage project; some of them work within the OCaml ecosystem (but not necessarily Mirage), some work on system programming (not necessarily in OCaml). The whole place is for all of us for one week, ex…

Between March 6th and March 13th 2019, I attended the Mirage retreat organized by Hannes Mehnert in Marrakesh, Morocco.

The Mirage retreat takes place in an artist residency organized as a hostel (shared rooms with simple beds). Hannes gathers a lot of people whose activity is relevant to the Mirage project; some of them work within the OCaml ecosystem (but not necessarily Mirage), some work on system programming (not necessarily in OCaml). The whole place is for all of us for one week, excellent food is provided, and we get to do whatever we want. (Thanks to the work of the people there who make this possible.)

This was my second time attending the retreat – first time in November 2017. It is probably the work-related trip I enjoy most. When I get back home, I’m exhausted, thrilled, I met fascinating people and I learned a lot.

Marracheck

This week I came with a specific project (that was decided spontaneously maybe three weeks before that): I would work with Armaël Guéneau, also attending the retreat, on mixing ideas for the existing tools to check opam packages (opam-builder, opamcheck, opam-health-check), with the objective of building a tool that can build the whole opam-repository is less than a day on my laptop machine. The ultimate goal is to make it extremely easy for anyone to test the impact of a change to the OCaml compiler on the OCaml ecosystem.

We started with a lot of discussions on the design, inspired by our knowledge of opam-builder and opamcheck – I had hacked on opam-builder a bit before, and had detailed discussion with Damien about the design of opamcheck – and discussions with Kate, working on opam-health-check and in general the opam CI, also attending the retreat. Then we did a good bit of pair-programming, with Armaël behind the keyboard. We decided to rebuild a tool from scratch and to use the opam-libs (the library-level API of the opam codebase). By the end of the week, we were still quite far from a working release, but we have a skeleton in place.

This would not have been possible without the presence, at the retreat, of Louis Gesbert and Raja Boujbel, who helped us navigating the (sometimes daunting) opam API. (We also noticed a few opportunities for improvements and sent a couple pull-requests to opam itself.) Louis and Raja are impressive in their handling of the opam codebase. There are obscure and ugly and painful things within the opam APIs, but they come from elegance/simplicity/pragmatism compromises that they made, understand well, and are consistently able to justify. It feels like a complex codebase that is growing as it discovers its use-cases, with inevitable cruft, but good hands at work to manage this complexity, within resource limits.

Network drivers

My roommate was Fabian Bonk, who participated to the “ixy project”, at the TUM (Technische Universität München), Munich, Germany. The "ixy project’ aims to implement a simple userland network driver (for some specific Intel network card) in many different languages, and see what work and what doesn’t. Fabian wrote the OCaml implementation, and was interested in finding ways to improve its performances.

At first I preferred to hear about his work from a distance; I know nothing of network card, and there were people at the retreat noticeably more knowledgeable about writing high-performance OCaml code. Then I realized that this was a dangerous strategy: for essientally any topic there is someone more knowledgeable than you at the retreat. So why not work on userland network drivers?

Fabian and I made a few attempts at making the program faster, which had the somewhat hilarious result of making the program about 500x slower. It’s an interesting problem domain. The driver author says “I would really need to remove this copy here, even though that would require changing the whole Mirage API”; the first reaction is to argue that copying memory is actually quite fast, so it’s probably not the bottleneck. “But we have to copy”, they say, “ten gibibytes per second!”. Ouch.

Anyway, after some tinkering, I realized that Fabian working over SSH to a machine in Munich with the network card, and being able to run latency tests because “for this you need an optical splitter and I don’t have the privilege level to access the one our university has”, wasn’t that great for benchmarking. So I decided to convince Fabian to implement a compliant network card, in C, on his machine – he insists on calling it a “simulator” but what’s the difference between software and hardware these days? The idea was, anyone could then use his network card on their own machine to test and benchmark the driver against, and make it faster. Unfortunately, he had an OSX machine, and everything you would need to implement this nicely is sort of broken on OSX (working POSIX-compliant shared memory? nope!).

Crowbar

One thing I realized during the retreat is that I have an amazing (dis)advantage over some other people there (Hannes included): I know that Crowbar is extremely easy to use. (You write a generator, a quickcheck-style test, you listen to the tool tell you how to set a few weird environment variables, and boom, there come the bugs.)

Apparently people who haven’t tried Crowbar yet are unwilling to do so because they’re not sure how easy it is. Unfortunately, having the amazing power to find bugs is also a curse: Hannes persuaded me to write a test for an OCaml implementation of the patch utility instead of sleeping one evening.

I’m not sure what tool authors can do to reduce this particular barrier to entry. Maybe one thing that works is to simply demo the tool in front of a crowded audience, every time you have a chance.

Mystery in a box

I helped Antonio Monteiro track down a failure in his HTTP/2 implementation, and over the course of that I caught a glimpse of the angstrom codebase. Angstrom contains a single-field record (used for first-class polymorphism) in one apparently-central data structure, and I noticed that the record does not carry the [@@unboxed] annotation (so it is one extra indirection at runtime). So I decided to add the annotation, hoping it would improve performances.

There is a dirty secret about [@@unboxed]: despite what most people think, it is extremely rare that it can make programs noticeably faster, because the GC is quite fast and combines allocations together – many allocations of a boxed object are combined with an allocation for their content or container, and and often the indirection points to an immediately adjacent place in memory so is basically free to dereference. It may help in some extreme low-latency scenario where code is written to not allocate at all, but I have never personally seen a program where [@@unboxed] makes a noticeable performance difference.

That is, until angstrom. Adding [@@unboxed] to this record field makes the program noticeably slower. The generated code, at the point where this record is used, is much nicer, each run allocates less words, but the program is noticeably slower – 7% slower. I found it extremely puzzling; Romain @dinosaure Calabiscetta pointed out that he tried the same thing, and was similarly puzzled.

Eventually I lured Pierre Chambart into studying the problem with me, and we figured it out. I won’t get into the technical details here (hopefully later), but I’ll point out that we tested our hypothesis by inserting (); in several places in the program, and Armaël’s baffled look made it more than worthwhile.

Video games

When invited to work on “anything they wanted”, some people had a projects that sounded a bit more fun than a parallel compiler of all OPAM packages – a gameboy emulator, for example. Of course, everyone knows that having fun side-projects to work on from time to time is an excellent thing. Yet those were kept in the recent past after more pressing side-projects on my TODO list (typically releasing ocamlbuild, batteries, ppx_deriving and plugins once in a while, or reviewing a compiler Pull Request). While no one was working on that specifically, this retreat made me want to try (eventually) something that I’ve never done before, namely implement a video game in OCaml. We’ll see whether that happens someday.

Conclusion

Thanks to everyone who was at the retreat (including the people that worked hard to ensure we could be there in the best condition). I had a great time and I’m hoping to come again for one of the next retreats.

We are pleased to announce the release of opam 2.0.4.

This new version contains some backported fixes:

• Sandboxing on macOS: considering the possibility that TMPDIR is unset [#3597 @herbelin – fix #3576]
• display: Fix opam config var display, aligned on opam config list [#3723 @rjbou – rel. #3717]
• pin:
  • update source of (version) pinned directory [#3726 @rjbou – fix #3651]
  • fix --ignore-pin-depends with autopin [#3736 @AltGr]
  • fix pinnings not installing/upgrading already pinned p…

We are pleased to announce the release of opam 2.0.4.

This new version contains some backported fixes:

• Sandboxing on macOS: considering the possibility that TMPDIR is unset [#3597 @herbelin – fix #3576]
• display: Fix opam config var display, aligned on opam config list [#3723 @rjbou – rel. #3717]
• pin:
  • update source of (version) pinned directory [#3726 @rjbou – fix #3651]
  • fix --ignore-pin-depends with autopin [#3736 @AltGr]
  • fix pinnings not installing/upgrading already pinned packages (introduced in 2.0.2) [#3800 @AltGr]
• opam clean: Ignore errors trying to remove directories [#3732 @kit-ty-kate]
• remove wrong “mismatched extra-files” warning [#3744 @rjbou]
• urls: fix hg opam 1.2 url parsing [#3754 @rjbou]
• lint: update message of warning 47, to avoid confusion because of missing synopsis field internally inferred from descr [#3753 @rjbou – fix #3738]
• system:
  • lock & signals: don’t interrupt at non terminal signals [#3541 @rjbou]
  • shell: fix fish manpath setting [#3728 @gregory-nisbet]
  • git: use diff.noprefix=false config argument to overwrite user defined configuration [#3788 @rjbou, #3628 @Blaisorblade – fix #3627]
• dirtrack: fix precise tracking mode [#3796 @rjbou]
• fix some mispellings [#3731 @MisterDA]
• CI enhancement & fixes [#3706 @dra27, #3748 @rjbou, #3801 @rjbou]

Note: To homogenise macOS name on system detection, we decided to keep macos, and convert darwin to macos in opam. For the moment, to not break 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. Please head to the latter for the comments!

We are pleased to announce the release of opam 2.0.4.

This new version contains some backported fixes:

• Sandboxing on macOS: considering the possibility that TMPDIR is unset [#3597 @herbelin - fix #3576]
• display: Fix opam config var display, aligned on opam config list [#3723 @rjbou - rel. #3717]
• pin:
  • update source of (version) pinned directory [#3726 @rjbou - #3651]
  • fix --ignore-pin-depends with autopin [#3736 @AltGr]
  • fix pinnings not installing/upgrading already pinned packages (introduced in 2.0.…

We are pleased to announce the release of opam 2.0.4.

This new version contains some backported fixes:

• Sandboxing on macOS: considering the possibility that TMPDIR is unset [#3597 @herbelin - fix #3576]
• display: Fix opam config var display, aligned on opam config list [#3723 @rjbou - rel. #3717]
• pin:
  • update source of (version) pinned directory [#3726 @rjbou - #3651]
  • fix --ignore-pin-depends with autopin [#3736 @AltGr]
  • fix pinnings not installing/upgrading already pinned packages (introduced in 2.0.2) [#3800 @AltGr]
• opam clean: Ignore errors trying to remove directories [#3732 @kit-ty-kate]
• remove wrong "mismatched extra-files" warning [#3744 @rjbou]
• urls: fix hg opam 1.2 url parsing [#3754 @rjbou]
• lint: update message of warning 47, to avoid confusion because of missing synopsis field internally inferred from descr [#3753 @rjbou - fix #3738]
• system:
  • lock & signals: don't interrupt at non terminal signals [#3541 @rjbou]
  • shell: fix fish manpath setting [#3728 @gregory-nisbet]
  • git: use diff.noprefix=false config argument to overwrite user defined configuration [#3788 @rjbou, #3628 @Blaisorblade - fix #3627]
• dirtrack: fix precise tracking mode [#3796 @rjbou]
• fix some mispellings [#3731 @MisterDA]
• CI enhancement & fixes [#3706 @dra27, #3748 @rjbou, #3801 @rjbou]

Note: To homogenise macOS name on system detection, we decided to keep macos, and convert darwin to macos in opam. For the moment, to not break 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. Please head to the latter for the comments!

Tarides is pleased to have contributed to the dune 1.9.0 release which introduces the concept of library variants. Thanks to this update, unikernels builds are becoming easier and faster in the MirageOS universe! This also opens the door for a better cross-compilation story, which will ease the addition of new MirageOS backends (trustzone, ESP32, RISC-V, etc.)

This post has also been posted to the Dune blog. See also the the discuss forum for more details.

Dune 1.9.0

Changes include:

• Coloring …

Tarides is pleased to have contributed to the dune 1.9.0 release which introduces the concept of library variants. Thanks to this update, unikernels builds are becoming easier and faster in the MirageOS universe! This also opens the door for a better cross-compilation story, which will ease the addition of new MirageOS backends (trustzone, ESP32, RISC-V, etc.)

This post has also been posted to the Dune blog. See also the the discuss forum for more details.

Dune 1.9.0

Changes include:

• Coloring in the watch mode (#1956)
• $ dune init command to create or update project boilerplate (#1448)
• Allow "." in c_names and cxx_names (#2036)
• Experimental Coq support
• Support for library variants and default implementations (#1900)

Variants

In dune 1.7.0, the concept of virtual library was introduced: https://dune.build/blog/virtual-libraries/. This feature allows to mark some abstract library as virtual, and then have several implementations for it. These implementations could be for multiple targets (unix, xen, js), using different algorithms, using C code or not. However each implementation in a project dependency tree had to be manually selected. Dune 1.9.0 introduces features for automatic selection of implementations.

Library variants

Variants is a tagging mechanism to select implementations on the final linking step. There's not much to add to make your implementation use variants. For example, you could decide to design a bar_js library which is the javascript implementation of bar, a virtual library. All you need to do is specificy a js tag using the variant option.

(library
 (name bar_js)
 (implements bar)
 (variant js)); <-- variant specification

Now any executable that depend on bar can automatically select the bar_js library variant using the variants option in the dune file.

(executable
 (name foo)
 (libraries bar baz)
 (variants js)); <-- variants selection

Common variants

Language selection

In your projects you might want to trade off speed for portability:

• ocaml: pure OCaml
• c: OCaml accelerated by C

JavaScript backend

• js: code aiming for a Node backend, using Js_of_ocaml

Mirage backends

The Mirage project (mirage.io) will make extensive use of this feature in order to select the appropriate dependencies according to the selected backend.

• unix: Unikernels as Unix applications, running on top of mirage-unix
• xen: Xen backend, on top of mirage-xen
• freestanding: Freestanding backend, on top of mirage-solo5

Default implementation

To facilitate the transition from normal libraries into virtuals ones, it's possible to specify an implementation that is selected by default. This default implementation is selected if no implementation is chosen after variant resolution.

(library
 (name bar)
 (virtual_modules hello)
 (default_implementation bar_unix)); <-- default implementation selection

Selection mechanism

Implementation is done with respect to some priority rules:

• manual selection of an implementation overrides everything
• after that comes selection by variants
• finally unimplemented virtual libraries can select their default implementation

Libraries may depend on specific implementations but this is not recommended. In this case, several things can happen:

• the implementation conflicts with a manually selected implementation: resolution fails.
• the implementation overrides variants and default implementations: a cycle check is done and this either resolves or fails.

Conclusion

Variant libraries and default implementations are fully documented here. This feature improves the usability of virtual libraries.

This commit shows the amount of changes needed to make a virtual library use variants.

Coq support

Dune now supports building Coq projects. To enable the experimental Coq extension, add (using coq 0.1) to your dune-project file. Then, you can use the (coqlib ...) stanza to declare Coq libraries.

A typical dune file for a Coq project will look like:

(include_subdirs qualified) ; Use if your development is based on sub directories

(coqlib
  (name Equations)                  ; Name of wrapper module
  (public_name equations.Equations) ; Generate an .install file
  (synopsis "Equations Plugin")     ; Synopsis
  (libraries equations.plugin)      ; ML dependencies (for plugins)
  (modules :standard \ IdDec)       ; modules to build
  (flags -w -notation-override))    ; coqc flags

See the documentation of the extension for more details.

Credits

This release also contains many other changes and bug fixes that can be found on the discuss announce.

Special thanks to dune maintainers and contributors for this release: @rgrinberg, @emillon, @shonfeder and @ejgallego!

MirageOS Spring Hack Retreat, Marrakesh 2019

Early March 2019, 31 MirageOS hackers gathered again in Marrakesh for our bi-annual hack retreat. We'd like to thank our amazing hosts, and everyone who participated on-site or remotely, and especially those who wrote up their experiences.

On this retreat, we ate our own dogfood, and used our MirageOS DHCP, recursive DNS resolver, and CalDAV unikernels as isolated virtual machines running on a PC Engines APU with FreeBSD as host system. The CalDAV s…

MirageOS Spring Hack Retreat, Marrakesh 2019

Early March 2019, 31 MirageOS hackers gathered again in Marrakesh for our bi-annual hack retreat. We'd like to thank our amazing hosts, and everyone who participated on-site or remotely, and especially those who wrote up their experiences.

On this retreat, we ate our own dogfood, and used our MirageOS DHCP, recursive DNS resolver, and CalDAV unikernels as isolated virtual machines running on a PC Engines APU with FreeBSD as host system. The CalDAV server persisted its data in a git repository on the host system, using the raw git protocol for communication, the smart HTTP protocol could have been used as well. Lynxis wrote a detailed blog post about our uplink situation.

Lots of interesting discussions took place, code was developed, knowledge was exchanged, and issues were solved while we enjoyed the sun and the Moroccan food. The following list is not exhaustive, but gives an overview what was pushed forward.

Imagelib

Imagelib is a library that can parse several image formats, and eye-of-mirage uses it to display those images in a framebuffer.

During the retreat, imagelib was extended with support for the BMP format, it's build system was revised to split off Unix-dependent functionality, and preliminary support for the GIF format was implemented.

ActivityPub

ActivityPub is an open, decentralized social networking protocol, as used by mastodon. It provides a client/server API for creating, updating, and deleting content, and a federated server-to-server API for notifications and content delivery. During the retreat, an initial prototype of a protocol implementation was drafted.

opam

Opam, the OCaml package manager, was extended in several directions:

• External (OS package system) dependency integration
• Interleaving download with build/install actions
• Generalisation of the job scheduler
• JSON serialisation, including crowbar round-trip tests
• Plugin evaluating (binary) reproducibility of opam packages
• some smaller cleanup PRs (return values, locking code)

marracheck

Work was started on a new utility to install as many opam packages as possible on a machine (there just wasn't enough choice with opam-builder, opamcheck and opam-check-all). It uses opam-lib and Z3 to accomplish this.

Conex

Conex is used for signing community repositories, esp. the opam-repository. Any opam package author can cryptographically sign their package releases, and users can verify that the downloaded tarball and build instructions are identical to what the author intended.

Conex has been developed since 2015, but is not yet widely deployed. We extended opam-publish to invoke the conex_targets utility and sign before opening a pull request on the opam-repository.

SMTP

The simple mail transfer protocol is an Internet standard for sending and receiving eMail. Our OCaml implementation has been improved, and it is possible to send eMails from OCaml code now.

HTTP2

The hypertext transfer protocol is an Internet standard widely used for browsing the world wide web. HTTP 1.1 is a line-based protocol which was specified 20 years ago. HTTP2 is an attempt to fix various shortcomings, and uses a binary protocol with multiplexing, priorities, etc. An OCaml implementation of HTTP2 has been actively worked on in Marrakesh.

Irmin

Irmin is a distributed database that follows the same design principles as git. Soon, Irmin 2.0 will be released, which includes GraphQL, HTTP, chunk support, and can use the git protocol for interoperability. Irmin provides a key-value interface for MirageOS.

OCaml compiler

Some hints on type errors for int literals and int operators were developed and merged to the OCaml compiler.

# 1.5 +. 2;;
         ^
Error: This expression has type int but an expression was expected of type
         float
       Hint: Did you mean `2.'?

# 1.5 + 2.;;
  ^^^ ^
Error: This expression has type float but an expression was expected of type
         int
Line 1, characters 4-5:
  Hint: Did you mean to use `+.'?

Also, the whole program dead code elimination PR was rebased onto trunk.

BGP / lazy trie

The mrt-format library which can parse multi-threaded routing toolkit traces, has been adapted to the modern OCaml ecosystem. The border gateway protocol (BGP) library was slightly updated, one of its dependencies, lazy-trie was adapted to the modern ecosystem as well.

Xen PVH

Xen provides several modes for virtualization. MirageOS's first non-Unix target was the para-virtualized (PV) mode for Xen, which does not require hardware support from the hypervisor's host operating system but has a weak security profile (static mapping of addresses, large attack surface). However, PV mode provides an attractive target for unikernels because it provides a simple software-based abstraction for dealing with drivers and a simple memory model; this is in contrast to hardware-virtualization mode, which provides greater security but requires more work from the guest OS.

A more modern virtualization mode combining the virtues of both approaches is PVH (formerly referred to as HVMLite), which is not yet supported by MirageOS. Marek Marczykowski-Górecki from the QubesOS project visited to help us bring PVH support to the unikraft project, a common platform for building unikernels which we hope to use for MirageOS's Xen support in the future.

During the retreat, lots of bugs porting MirageOS to PVH were solved. It boots and crashes now!

Learn OCaml as a unikernel

The platform learn OCaml embeds an editor, top-level, and exercises into a HTTP server, and allows students to learn OCaml, and submit solutions via the web interface, where an automated grader runs unit tests etc. to evaluate the submitted solutions. Teachers can assign mandatory exercises, and have an overview how the students are doing. Learn OCaml used to be executable only on a Unix host, but is now beeing ported into a MirageOS unikernel, executable as a standalone virtual machine.

Network device driver (ixy)

The ixy network driver supports Intel 82599 network interface cards, and is implemented in OCaml. Its performance has been improved, including several failing attempts which degraded its performance. Also, it has been integrated into the mirage tool and is usable as a mirage-net implementation.

DNS client API

Our proposed API is described here. Unix, Lwt, and MirageOS implementations are already available.

mirage-http unified HTTP API

Since we now have two HTTP servers, cohttp and httpaf, in OCaml and MirageOS available, the new interface mirage-http provides a unified interface, and also supports connection upgrades to websockets.

cstruct capabilities

We use cstruct, a wrapper around OCaml's Bigarray, quite a lot in MirageOS. Until now, cstruct is a readable and writable byte array. We used phantom types to add capabilities to the interface to distinct read-only and write-only buffers.

patch

An OCaml implementation to apply unified diffs. This code has been extracted from conex (since we found some issues in it), and still needs to be fixed.

Statistical memory profiler

Since 2016, Jacques-Henri Jourdan has been working on a statistical memory profiler for OCaml (read the OCaml 2016 paper). An Emacs user interface is available since some years. We integrated statmemprof into MirageOS unikernels using the statmemprof-mirage library, marshal the data via TCP, and provide a proxy that communicates with Emacs over a Unix domain socket, and the unikernel.

P2Pcollab

P2Pcollab is a collection of composable libraries implementing protocols for P2P collaboration. So far various P2P gossip protocols has been implemented. At this retreat the focus was on a gossip-based publish-subscribe dissemination protocol. Future plans include building P2P unikernels and adding P2P pub/sub sync functionality to Irmin.

It has been 3 months since I joined IIT Madras and it has been good fun so far. Along with the members of the RISE group, we’ve initiated a project to build secure applications on top of secure extensions of the open-source Shakti RISC-V processor ecosystem. Unsurprisingly, my language of choice to build the applications is OCaml. Given the availability of rich ecosystem of libraries under the MirageOS library operating system for building unikernels, we hope to minimise the amount of unsafe C…

It has been 3 months since I joined IIT Madras and it has been good fun so far. Along with the members of the RISE group, we’ve initiated a project to build secure applications on top of secure extensions of the open-source Shakti RISC-V processor ecosystem. Unsurprisingly, my language of choice to build the applications is OCaml. Given the availability of rich ecosystem of libraries under the MirageOS library operating system for building unikernels, we hope to minimise the amount of unsafe C code that the hardware has to contend with and protect exploits against. As a first step, we have managed to get OCaml programs to run on directly on top of the Shakti processor running in simulation under QEMU and Spike ISA simulators without an intervening operating system.

A custom bootloader performs the necessary hardware initialisation and transfers control directly to the OCaml program. We have open-sourced all of the tools necessary to build your own kernel. This handy dockerfile documents the entire process. For the impatient, an image is available in the dockerhub:

$ docker run -it iitmshakti/riscv-ocaml-baremetal:0.1.0

# Write your program
$ echo 'let _ = print_endline "A camel treads on hardware!"' > hello.ml
# Compile for Shakti
$ ocamlopt -output-obj -o payload.o hello.ml
$ file payload.o
payload.o: ELF 64-bit LSB relocatable, UCB RISC-V, version 1 (SYSV), not stripped

# Link with bootcode and build the kernel
$ make -C ../build
make: Entering directory '/root/ocaml-baremetal-riscv/build'
make[1]: Entering directory '/root/ocaml-baremetal-riscv/build'
make[2]: Entering directory '/root/ocaml-baremetal-riscv/build'
make[2]: Leaving directory '/root/ocaml-baremetal-riscv/build'
[ 64%] Built target boot
make[2]: Entering directory '/root/ocaml-baremetal-riscv/build'
make[2]: Leaving directory '/root/ocaml-baremetal-riscv/build'
[ 78%] Built target freestanding-compat
make[2]: Entering directory '/root/ocaml-baremetal-riscv/build'
make[2]: Leaving directory '/root/ocaml-baremetal-riscv/build'
[ 85%] Built target asmrun_t
make[2]: Entering directory '/root/ocaml-baremetal-riscv/build'
make[2]: Leaving directory '/root/ocaml-baremetal-riscv/build'
[ 92%] Built target nolibc_t
make[2]: Entering directory '/root/ocaml-baremetal-riscv/build'
make[2]: Leaving directory '/root/ocaml-baremetal-riscv/build'
[100%] Built target kernel
make[1]: Leaving directory '/root/ocaml-baremetal-riscv/build'
make: Leaving directory '/root/ocaml-baremetal-riscv/build'
$ file kernel 
kernel: ELF 64-bit LSB executable, UCB RISC-V, version 1 (SYSV), statically linked, with debug_info, not stripped

# Run under spike RISC-V ISA simulator
$ spike kernel
ocaml-boot: heap@0x80042be8 stack@0x8002fbc0
A camel treads on hardware!
ocaml-boot: caml runtime returned. shutting down!

# Run under QEMU
$ qemu-system-riscv64 -machine spike_v1.10 -smp 1 -m 1G -serial stdio -kernel kernel
VNC server running on 127.0.0.1:5900
ocaml-boot: heap@0x80042be8 stack@0x8002fbc0
A camel treads on hardware!
ocaml-boot: caml runtime returned. shutting down!

The immediate next step will be getting the code to run on a Shakti softcore on an FPGA. In addition to targeting high-end FPGAs, we will also be targeting the $100 Arty A7 hobbyist board and release all of the software under liberal open-source licenses.

Further along, we will port mirage libraries to Shakti following similar to the setup in Well-typed lightbulbs and implementing hardware security enhancements in Shakti for preventing spatial and temporal attacks while running unsafe C code (with the ability to dynamically turn it off when running OCaml!), hardware-assisted compartments, etc. Lots of exciting possibilities on the horizon!

Acknowledgements

Much of this work was done by the incredible Malte, who is a visiting student at IIT Madras on a semester away from Leibniz University Hannover, Arjun, Lavanya, Ambika, Chester, and the rest of the Shakti team. The RISC-V port of OCaml is developed and maintained by Nicolás Ojeda Bär.

We are pleased to announce the release of OCamlFormat (available on opam). There have been numerous changes since the last release, so here is a comprehensive list of the new features and breaking changes to help the transition from OCamlFormat 0.8.

Additional dependencies

OCamlFormat now requires:

• ocaml >= 4.06 (up from 4.04.1)
• dune >= 1.1.1
• octavius >= 1.2.0
• uutf

OCamlFormat_Reason now requires:

• ocaml >= 4.06
• dune >= 1.1.1
• ocaml-migrate-parsetree >= 1.0.10 (up from 1.0.6)
• octav…

We are pleased to announce the release of OCamlFormat (available on opam). There have been numerous changes since the last release, so here is a comprehensive list of the new features and breaking changes to help the transition from OCamlFormat 0.8.

Additional dependencies

OCamlFormat now requires:

• ocaml >= 4.06 (up from 4.04.1)
• dune >= 1.1.1
• octavius >= 1.2.0
• uutf

OCamlFormat_Reason now requires:

• ocaml >= 4.06
• dune >= 1.1.1
• ocaml-migrate-parsetree >= 1.0.10 (up from 1.0.6)
• octavius >= 1.2.0
• uutf
• reason >= 3.2.0 (up from 1.13.4)

New preset profiles

The ocamlformat profile aims to take advantage of the strengths of a parsetree-based auto-formatter, and to limit the consequences of the weaknesses imposed by the current implementation. This is a style which optimizes for what the formatter can do best, rather than to match the style of any existing code. General guidelines that have directed the design include:

• Legibility, in the sense of making it as hard as possible for quick visual parsing to give the wrong interpretation, is of highest priority;
• Whenever possible the high-level structure of the code should be obvious by looking only at the left margin, in particular, it should not be necessary to visually jump from left to right hunting for critical keywords, tokens, etc;
• All else equal compact code is preferred as reading without scrolling is easier, so indentation or white space is avoided unless it helps legibility;
• Attention has been given to making some syntactic gotchas visually obvious. ocamlformat is the new default profile.

The conventional profile aims to be as familiar and \"conventional\" appearing as the available options allow.

The default profile is ocamlformat with break-cases=fit. default is deprecated and will be removed in version 0.10.

OCamlFormat diff tool

ocamlformat-diff is a tool that uses OCamlFormat to apply the same formatting to compared OCaml files, so that the formatting differences between the two files are not displayed. Note that ocamlformat-diff comes in a separate opam package and is not included in the ocamlformat package.

The file comparison is then performed by any diff backend.

The options' documentation is available through ocamlformat-diff --help.

The option --diff allows you to configure the diff command that is used to compare the formatted files. The default value is the vanilla diff, but you can also use patdiff or any other similar comparison tool.

ocamlformat-diff can be integrated with git diff, as explained in the online documentation.

Formatting docstrings

Previously, the docstrings (** This is a docstring *) could only be formatted like regular comments, a new option --parse-docstrings has been added so that docstrings can be nicely formatted.

Here is a small example:

(** {1 Printers and escapes used by Cmdliner module} *)

val subst_vars : subst:(string -> string option) -> Buffer.t -> string -> string
(** [subst b ~subst s], using [b], substitutes in [s] variables of the form
    "$(doc)" by their [subst] definition. This leaves escapes and markup
    directives $(markup,...) intact.
    @raise Invalid_argument in case of illegal syntax. *)

Note that this option is disabled by default and you have to set it manually by adding --parse-docstrings to your command line or parse-docstrings=true to your .ocamlformat file. If you get the following error message:

Error: Formatting of (** ... *) is unstable (e.g. parses as a list or not depending on the margin), please tighten up this comment in the source or disable the formatting using the option --no-parse-docstrings.

It means the original docstring cannot be formatted (e.g. because it does not comply with the odoc syntax) and you have to edit it or disable the formatting of docstrings.

Of course if you think your docstring complies with the odoc syntax and there might be a bug in OCamlFormat, feel free to file an issue on github.

Print the configuration

The new --print-config flag prints the configuration determined by the environment variable, the configuration files, preset profiles and command line. Attributes are not considered.

It provides the full list of options with the values they are set to, and the source of this value. For example ocamlformat --print-config prints:

profile=ocamlformat (file .ocamlformat:1)
quiet=false (profile ocamlformat (file .ocamlformat:1))
max-iters=10 (profile ocamlformat (file .ocamlformat:1))
comment-check=true (profile ocamlformat (file .ocamlformat:1))
wrap-fun-args=true (profile ocamlformat (file .ocamlformat:1))
wrap-comments=true (file .ocamlformat:5)
type-decl=compact (profile ocamlformat (file .ocamlformat:1))
space-around-collection-expressions=false (profile ocamlformat (file .ocamlformat:1))
single-case=compact (profile ocamlformat (file .ocamlformat:1))
sequence-style=separator (profile ocamlformat (file .ocamlformat:1))
parse-docstrings=true (file .ocamlformat:4)
parens-tuple-patterns=multi-line-only (profile ocamlformat (file .ocamlformat:1))
parens-tuple=always (profile ocamlformat (file .ocamlformat:1))
parens-ite=false (profile ocamlformat (file .ocamlformat:1))
ocp-indent-compat=false (profile ocamlformat (file .ocamlformat:1))
module-item-spacing=sparse (profile ocamlformat (file .ocamlformat:1))
margin=77 (file .ocamlformat:3)
let-open=preserve (profile ocamlformat (file .ocamlformat:1))
let-binding-spacing=compact (profile ocamlformat (file .ocamlformat:1))
let-and=compact (profile ocamlformat (file .ocamlformat:1))
leading-nested-match-parens=false (profile ocamlformat (file .ocamlformat:1))
infix-precedence=indent (profile ocamlformat (file .ocamlformat:1))
indicate-nested-or-patterns=space (profile ocamlformat (file .ocamlformat:1))
indicate-multiline-delimiters=true (profile ocamlformat (file .ocamlformat:1))
if-then-else=compact (profile ocamlformat (file .ocamlformat:1))
field-space=tight (profile ocamlformat (file .ocamlformat:1))
extension-sugar=preserve (profile ocamlformat (file .ocamlformat:1))
escape-strings=preserve (profile ocamlformat (file .ocamlformat:1))
escape-chars=preserve (profile ocamlformat (file .ocamlformat:1))
doc-comments-tag-only=default (profile ocamlformat (file .ocamlformat:1))
doc-comments-padding=2 (profile ocamlformat (file .ocamlformat:1))
doc-comments=after (profile ocamlformat (file .ocamlformat:1))
disable=false (profile ocamlformat (file .ocamlformat:1))
cases-exp-indent=4 (profile ocamlformat (file .ocamlformat:1))
break-struct=force (profile ocamlformat (file .ocamlformat:1))
break-string-literals=wrap (profile ocamlformat (file .ocamlformat:1))
break-sequences=false (profile ocamlformat (file .ocamlformat:1))
break-separators=before (profile ocamlformat (file .ocamlformat:1))
break-infix-before-func=true (profile ocamlformat (file .ocamlformat:1))
break-infix=wrap (profile ocamlformat (file .ocamlformat:1))
break-fun-decl=wrap (profile ocamlformat (file .ocamlformat:1))
break-collection-expressions=fit-or-vertical (profile ocamlformat (file .ocamlformat:1))
break-cases=fit (file .ocamlformat:2)

If many input files are specified, only print the configuration for the first file. If no input file is specified, print the configuration for the root directory if specified, or for the current working directory otherwise.

Parentheses around if-then-else branches

A new option parens-ite has been added to decide whether to use parentheses around if-then-else branches that spread across multiple lines.

If this option is set, the following function:

let rec loop count a =
  if count >= self#len
  then a
  else
    let a' = f cur#get count a in
    cur#incr ();
    loop (count + 1) a'

will be formatted as:

let rec loop count a =
  if count >= self#len
  then a
  else (
    let a' = f cur#get count a in
    cur#incr ();
    loop (count + 1) a' )

Parentheses around tuple patterns

A new option parens-tuple-patterns has been added, that mimics parens-tuple but only applies to patterns, whereas parens-tuples only applies to expressions. parens-tuple-patterns=multi-line-only mode will try to skip parentheses for single-line tuple patterns, this is the default value. parens-tuple-patterns=always always uses parentheses around tuples patterns.

For example:

(* with parens-tuple-patterns=always *)
let (a, b) = (1, 2)

(* with parens-tuple-patterns=multi-line-only *)
let a, b = (1, 2)

Single-case pattern-matching expressions

The new option single-case defines the style of pattern-matching expressions with only a single case. single-case=compact will try to format a single case on a single line, this is the default value. single-case=sparse will always break the line before a single case.

For example:

(* with single-case=compact *)
try some_irrelevant_expression
with Undefined_recursive_module _ -> true

(* with single-case=sparse *)
try some_irrelevant_expression
with
| Undefined_recursive_module _ -> true

Space around collection expressions

The new option space-around-collection-expressions decides whether to add a space inside the delimiters of collection expressions (lists, arrays, records).

For example:

(* by default *)
type wkind = {f : 'a. 'a tag -> 'a kind}
let l = ["Nil", TCnoarg Thd; "Cons", TCarg (Ttl Thd, tcons)]

(* with space-around-collection-expressions *)
type wkind = { f : 'a. 'a tag -> 'a kind }
let l = [ "Nil", TCnoarg Thd; "Cons", TCarg (Ttl Thd, tcons) ]

Break separators

The new option break-separators decides whether to break before or after separators such as ; in list or record expressions, * in tuples or -> in arrow types. break-separators=before breaks the expressions before the separator, this is the default value. break-separators=after breaks the expressions after the separator. break-separators=after-and-docked breaks the expressions after the separator and docks the brackets for records.

For example:

(* with break-separators=before *)
type t =
  { foooooooooooooooooooooooo: foooooooooooooooooooooooooooooooooooooooo
  ; fooooooooooooooooooooooooooooo: fooooooooooooooooooooooooooo }

(* with break-separators=after *)
type t =
  { foooooooooooooooooooooooo: foooooooooooooooooooooooooooooooooooooooo;
    fooooooooooooooooooooooooooooo: fooooooooooooooooooooooooooo }

(* with break-separators=after-and-docked *)
type t = {
  foooooooooooooooooooooooo: foooooooooooooooooooooooooooooooooooooooo;
  fooooooooooooooooooooooooooooo: fooooooooooooooooooooooooooo
}

Not breaking before bind/map operators

The new option break-infix-before-func decides whether to break infix operators whose right arguments are anonymous functions specially. This option is set by default, if you disable it with --no-break-infix-before-func, it will not break before the operator so that the first line of the function appears docked at the end of line after the operator.

For example:

(* by default *)
f x
>>= fun y ->
g y
>>= fun () ->
f x >>= fun y -> g y >>= fun () -> f x >>= fun y -> g y >>= fun () -> y ()

(* with break-infix-before-func = false *)
f x >>= fun y ->
g y >>= fun () ->
f x >>= fun y -> g y >>= fun () -> f x >>= fun y -> g y >>= fun () -> y ()

Break toplevel cases

There is a new value for the break-cases option: toplevel, that forces top-level cases (i.e. not nested or-patterns) to break across lines, otherwise breaks naturally at the margin.

For example:

let f =
  let g = function
    | H when x y <> k -> 2
    | T | P | U -> 3
  in
  fun x g t h y u ->
    match x with
    | E -> 4
    | Z | P | M -> (
      match y with
      | O -> 5
      | P when h x -> (
          function
          | A -> 6 ) )

Number of spaces before docstrings

The new option doc-comments-padding controls how many spaces are printed before doc comments in type declarations. The default value is 2.

For example:

(* with doc-comments-padding = 2 *)
type t = {a: int  (** a *); b: int  (** b *)}

(* with doc-comments-padding = 1 *)
type t = {a: int (** a *); b: int (** b *)}

Ignore files

An .ocamlformat-ignore file specifies files that OCamlFormat should ignore. Each line in an .ocamlformat-ignore file specifies a filename relative to the directory containing the .ocamlformat-ignore file. Lines starting with # are ignored and can be used as comments.

Here is an example of such .ocamlformat-ignore file:

#This is a comment
dir2/ignore_1.ml

Tag-only docstrings

The new option doc-comments-tag-only controls the position of doc comments only containing tags. doc-comments-tag-only=default means no special treatment is done, this is the default value. doc-comments-tag-only=fit puts doc comments on the same line if it fits.

For example:

(* with doc-comments-tag-only = default *)

(** @deprecated  *)
open Module

(* with doc-comments-tag-only = fit *)

open Module (** @deprecated  *)

Fit or vertical mode for if-then-else

There is a new value for the option if-then-else: fit-or-vertical. fit-or-vertical vertically breaks all branches if they do not fit on a single line. Compared to the compact (default) value, it breaks all branches if at least one of them does not fit on a single line.

For example:

(* with if-then-else = compact *)
let _ =
  if foo then
    let a = 1 in
    let b = 2 in
    a + b
  else if foo then 12
  else 0

(* with if-then-else = fit-or-vertical *)
let _ =
  if foo then
    let a = 1 in
    let b = 2 in
    a + b
  else if foo then
    12
  else
    0

Check mode

A new --check flag has been added. It checks whether the input files already are formatted. This flag is mutually exclusive with --inplace and --output. It returns 0 if the input files are indeed already formatted, or 1 otherwise.

Break function declarations

The new option break-fun-decl controls the style for function declarations and types. break-fun-decl=wrap breaks only if necessary, this is the default value. break-fun-decl=fit-or-vertical vertically breaks arguments if they do not fit on a single line. break-fun-decl=smart is like fit-or-vertical but try to fit arguments on their line if they fit. The wrap-fun-args option now only controls the style for function calls, and no more for function declarations.

For example:

(* with break-fun-decl = wrap *)
let ffffffffffffffffffff aaaaaaaaaaaaaaaaaaaaaa bbbbbbbbbbbbbbbbbbbbbb
    cccccccccccccccccccccc =
  g

(* with break-fun-decl = fit-or-vertical *)
let ffffffffffffffffffff
    aaaaaaaaaaaaaaaaaaaaaa
    bbbbbbbbbbbbbbbbbbbbbb
    cccccccccccccccccccccc =
  g

(* with break-fun-decl = smart *)
let ffffffffffffffffffff
    aaaaaaaaaaaaaaaaaaaaaa bbbbbbbbbbbbbbbbbbbbbb cccccccccccccccccccccc =
  g

Disable configuration in files and attributes

Two new options have been added so that .ocamlformat configuration files and attributes in OCaml files do not change the configuration. These options can be useful if you use some preset profile and you do not want attributes and .ocamlformat files to interfere with your preset configuration. --disable-conf-attrs disables the configuration in attributes, and --disable-conf-files disables .ocamlformat configuration files.

Preserve module items spacing

There is a new value for the option module-item-spacing: preserve, that will not leave open lines between one-liners of similar sorts unless there is an open line in the input.

For example the line breaks are preserved in the following code:

let cmos_rtc_seconds = 0x00
let cmos_rtc_seconds_alarm = 0x01
let cmos_rtc_minutes = 0x02

let x = o

let log_other = 0x000001
let log_cpu = 0x000002
let log_fpu = 0x000004

Breaking changes

• When --disable-outside-detected-project is set, disable ocamlformat when no .ocamlformat file is found.
• Files are not parsed when ocamlformat is disabled.
• Disallow - with other input files.
• The wrap-fun-args option now only controls the style for function calls, and no more for function declarations.
• The default profile is now named ocamlformat.
• The deprecated syntax for .ocamlformat files: option value is no more supported anymore and you should use the option = value syntax instead.

Miscellaneous bugfixes

• Preserve shebang (e.g. #!/usr/bin/env ocaml) at the beginning of a file.
• Improve the formatting when ocp-indent-compat is set.
• UTF8 characters are now correctly printed in comments.
• Add parentheses around a constrained any-pattern (e.g. let (_ : int) = x1).
• Emacs: the temporary buffer is now killed.
• Emacs: add the keybinding in tuareg's map instead of merlin's.
• Lots of improvements on the comments, docstrings, attributes formatting.
• Lots of improvements on the formatting of modules.
• Lots of improvements in the Reason support.
• Do not rely on the file-system to format sources.
• The --debug mode is more user-friendly.

Credits

This release also contains many other changes and bug fixes that we cannot detail here.

Special thanks to our maintainers and contributors for this release: Jules Aguillon, Mathieu Barbin, Josh Berdine, Jérémie Dimino, Hugo Heuzard, Ludwig Pacifici, Guillaume Petiot, Nathan Rebours and Louis Roché.

If you wish to get involved with OCamlFormat development or file an issue, please read the contributing guide, any contribution is welcomed.

MirageOS Security Advisory 01 - memory disclosure in mirage-net-xen

• Module: netchannel
• Announced: 2019-03-21
• Credits: Thomas Leonard, Hannes Mehnert, Mindy Preston
• Affects: netchannel = 1.10.0
• Corrected: 2019-03-20 1.10.1 release

For general information regarding MirageOS Security Advisories, please visit https://mirage.io/security.

Background

MirageOS is a library operating system using cooperative multitasking, which can be executed as a guest of the Xen hypervisor. Virtu…

MirageOS Security Advisory 01 - memory disclosure in mirage-net-xen

• Module: netchannel
• Announced: 2019-03-21
• Credits: Thomas Leonard, Hannes Mehnert, Mindy Preston
• Affects: netchannel = 1.10.0
• Corrected: 2019-03-20 1.10.1 release

For general information regarding MirageOS Security Advisories, please visit https://mirage.io/security.

Background

MirageOS is a library operating system using cooperative multitasking, which can be executed as a guest of the Xen hypervisor. Virtual devices, such as a network device, share memory between MirageOS and the hypervisor. To maintain adequate performance, the virtual device managing network communication between MirageOS and the Xen hypervisor maintains a shared pool of pages and reuses them for write requests.

Problem Description

In version 1.10.0 of netchannel, the API for handling network requests changed to provide higher-level network code with an interface for writing into memory directly. As part of this change, code paths which exposed memory taken from the shared page pool did not ensure that previous data had been cleared from the buffer. This error resulted in memory which the user did not overwrite staying resident in the buffer, and potentially being sent as part of unrelated network communication.

The mirage-tcpip library, which provides interfaces for higher-level operations like IPv4 and TCP header writes, assumes that buffers into which it writes have been zeroed, and therefore may not explicitly write some fields which are always zero. As a result, some packets written with netchannel v1.10.0 which were passed to mirage-tcpip with nonzero data will have incorrect checksums calculated and will be discarded by the receiver.

Impact

This issue discloses memory intended for another recipient and corrupts packets. Only version 1.10.0 of netchannel is affected. Version 1.10.1 fixes this issue.

Version 1.10.0 was available for less than one month and many upstream users had not yet updated their own API calls to use it. In particular, no version of qubes-mirage-firewall or its dependency mirage-nat compatible with version 1.10.0 was released.

Workaround

No workaround is available.

Solution

Transmitting corrupt data and disclosing memory is fixed in version 1.10.1.

The recommended way to upgrade is:

opam update
opam upgrade netchannel

Or, explicitly:

opam upgrade
opam reinstall netchannel=1.10.1

Affected releases (version 1.10.0 of netchannel and mirage-net-xen) have been marked uninstallable in the opam repository.

Correction details

The following list contains the correction revision numbers for each affected branch.

Memory disclosure on transmit:

master: 6c7a13a5dae0f58dcc0653206a73fa3d8174b6d2

1.10.0: bd0382eabe17d0824c8ba854ec935d8a2e5f7489

References

netchannel

You can find the latest version of this advisory online at https://mirage.io/blog/MSA01.

This advisory is signed using OpenPGP, you can verify the signature by downloading our public key from a keyserver (gpg --recv-key 4A732D757C0EDA74), downloading the raw markdown source of this advisory from GitHub and executing gpg --verify 01.txt.asc.

This blog post looks back on some of the improvements in opam 2.0, and gives tips on the new workflows available.

Package development environment management

Opam 2.0 has been vastly improved to handle locally defined packages. Assuming you have a project ~/projects/foo, defining two packages foo-lib and foo-bin, you would have:

~/projects/foo
|-- foo-lib.opam
|-- foo-bin.opam
`-- src/ ...

(See also about computed dependency constraints for handling multiple package definitions with mutual co…

This blog post looks back on some of the improvements in opam 2.0, and gives tips on the new workflows available.

Package development environment management

Opam 2.0 has been vastly improved to handle locally defined packages. Assuming you have a project ~/projects/foo, defining two packages foo-lib and foo-bin, you would have:

~/projects/foo
|-- foo-lib.opam
|-- foo-bin.opam
`-- src/ ...

(See also about computed dependency constraints for handling multiple package definitions with mutual constraints)

Automatic pinning

The underlying mechanism is the same, but this is an interface improvement that replaces most of the opam 1.2 workflows based on opam pin.

The usual commands (install, upgrade, remove, etc.) have been extended to support specifying a directory as argument. So when working on project foo, just write:

cd ~/projects/foo
opam install .

and both foo-lib and foo-bin will get automatically pinned to the current directory (using git if your project is versioned), and installed. You may prefer to use:

opam install . --deps-only

to just get the package dependencies ready before you start hacking on it. See below for details on how to reproduce a build environment more precisely. Note that opam depext . will not work at the moment, which will be fixed in the next release when the external dependency handling is integrated (opam will still list you the proper packages to install for your OS upon failure).

If your project is versioned and you made changes, remember to either commit, or add --working-dir so that your uncommitted changes are taken into account.

Local switches

Opam 2.0 introduced a new feature called "local switches". This section explains what it is about, why, when and how to use them.

Opam switches allow to maintain several separate development environments, each with its own set of packages installed. This is particularly useful when you need different OCaml versions, or for working on projects with different dependency sets.

It can sometimes become tedious, though, to manage, or remember what switch to use with what project. Here is where "local switches" come in handy.

How local switches are handled

A local switch is simply stored inside a _opam/ directory, and will be selected automatically by opam whenever your current directory is below its parent directory.

NOTE: it's highly recommended that you enable the new shell hooks when using local switches. Just run opam init --enable-shell-hook: this will make sure your PATH is always set for the proper switch.

You will otherwise need to keep remembering to run eval $(opam env) every time you cd to a directory containing a local switch. See also how to display the current switch in your prompt

For example, if you have ~/projects/foo/_opam, the switch will be selected whenever in project foo, allowing you to tailor what it has installed for the needs of your project.

If you remove the switch dir, or your whole project, opam will forget about it transparently. Be careful not to move it around, though, as some packages still contain hardcoded paths and don't handle relocation well (we're working on that).

Creating a local switch

This can generally start with:

cd ~/projects/foo
opam switch create . --deps-only

Local switch handles are just their path, instead of a raw name. Additionally, the above will detect package definitions present in ~/projects/foo, pick a compatible version of OCaml (if you didn't explicitely mention any), and automatically install all the local package dependencies.

Without --deps-only, the packages themselves would also get installed in the local switch.

Using an existing switch

If you just want an already existing switch to be selected automatically, without recompiling one for each project, you can use opam switch link:

cd ~/projects/bar
opam switch link 4.07.1

will make sure that switch 4.07.1 is chosen whenever you are in project bar. You could even link to ../foo here, to share foo's local switch between the two projects.

Reproducing build environments

Pinnings

If your package depends on development versions of some dependencies (e.g. you had to push a fix upstream), add to your opam file:

depends: [ "some-package" ] # Remember that pin-depends are depends too
pin-depends: [
  [ "some-package.version" "git+https://gitfoo.com/blob.git#mybranch" ]
]

This will have no effect when your package is published in a repository, but when it gets pinned to its dev version, opam will first make sure to pin some-package to the given URL.

Lock-files

Dependency contraints are sometimes too wide, and you don't want to explore all the versions of your dependencies while developing. For this reason, you may want to reproduce a known-working set of dependencies. If you use:

opam lock .

opam will check what version of the dependencies are installed in your current switch, and explicit them in *.opam.locked files. opam lock is a plugin at the moment, but will get automatically installed when needed.

Then, assuming you checked these files into version control, any user can do

opam install . --deps-only --locked

to instruct opam to reproduce the same build environment (the --locked option is also available to opam switch create, to make things easier).

The generated lock-files will also contain added constraints to reproduce the presence/absence of optional dependencies, and reproduce the appropriate dependency pins using pin-depends. Add the --direct-only option if you don't want to enforce the versions of all recursive dependencies, but only direct ones.

Liquidity version 1.0

We are pleased to announce the release of the first major version of the Liquidity smart-contract language and associated tools.

Some of the highlights of this version are detailed below.

Multiple Entry Points

In the previous versions of Liquidity, smart contracts were limited to a single entry point (named main). But traditionally smart contracts executions path depend strongly on the parameter and in most cases they are completely distinct.

Having different entry points a…

Liquidity version 1.0

We are pleased to announce the release of the first major version of the Liquidity smart-contract language and associated tools.

Some of the highlights of this version are detailed below.

Multiple Entry Points

In the previous versions of Liquidity, smart contracts were limited to a single entry point (named main). But traditionally smart contracts executions path depend strongly on the parameter and in most cases they are completely distinct.

Having different entry points allows to separate code that do not overlap and which usually accomplish vastly different tasks. Encoding entry points with complex pattern matching constructs before was tedious and made the code not extremely readable. This new feature gives you readability and allows to call contracts in a natural way.

Internally, entry points are encoded with sum types and pattern matching so that you keep the strong typing guarantees that come over from Michelson. This means that you cannot call a typed smart contract with the wrong entry point or the wrong parameter (this is enforced statically by both the Liquidity typechecker and the Michelson typechecker).

Modules and Contract System

Organizing, encapsulating and sharing code is not always easy when you need to write thousand lines files. Liquidity now allows to write modules (which contain types and values/functions) and contracts (which define entry points in addition). Types and non-private values of contracts and modules in scope can be accessed by other modules and contracts.

You can even compile several files at once with the command line compiler, so that you may organize your multiple smart contract projects in libraries and files.

Polymorphism and Type Inference

Thanks to a new and powerful type inference algorithm, you can now get rid of almost all type annotations in the smart contracts.

Instead of writing something like

let%entry main (parameter : bool) (storage : int) =
  let ops = ([] : operation list) in
  let f (c : bool) = if not c then 1 else 2 in
  ops, f parameter

you can now write

let%entry main parameter _ =
  let ops = [] in
  let f c = if not c then 1 else 2 in
  ops, f parameter

And type inference works with polymorhpism (also a new feature of this release) so you can now write generic and reusable functions:

type 'a t = { x : 'a set; y : 'a }

let mem_t v = Set.mem v.y v.x

Inference also works with contract types and entry points.

ReasonML Syntax

We originally used a modified version of the OCaml syntax for the Liquidity language. This made the language accessible, almost for free, to all OCaml and functional language developers. The typing discipline one needs is quite similar to other strongly typed functional languages so this was a natural fit.

However this is not the best fit for everyone. We want to bring the power of Liquidity and Tezos to the masses so adopting a seemingly familiar syntax for most people can help a lot. With this new version of Liquidity, you can now write your smart contracts in both an OCaml-like syntax or a ReasonML-like one. The latter being a lot closer to Javascript on the surface, making it accessible to people that already know the language or people that write smart contracts for other platforms like Solidity/Ethereum.

You can see the full changelog as well as download the latest release and binaries at this address.

Don’t forget that you can also try all these new cool features and more directly in your browser with our online editor.

MirageOS 3.5.0 release

We are happy to announce our MirageOS 3.5.0 release. We didn't announce post 3.0.0 releases too well -- that's why this post tries to summarize the changes in the MirageOS ecosystem over the past two years. MirageOS consists of over 100 opam packages, lots of which are reused in other OCaml projects and deployments without MirageOS. These opam packages are maintained and developed further by lots of developers.

On the OCaml tooling side, since MirageOS 3.0.0 we did severa…

MirageOS 3.5.0 release

We are happy to announce our MirageOS 3.5.0 release. We didn't announce post 3.0.0 releases too well -- that's why this post tries to summarize the changes in the MirageOS ecosystem over the past two years. MirageOS consists of over 100 opam packages, lots of which are reused in other OCaml projects and deployments without MirageOS. These opam packages are maintained and developed further by lots of developers.

On the OCaml tooling side, since MirageOS 3.0.0 we did several major changes:

• moved most packages to dune (formerly jbuilder) and began using dune-release for smooth developer experience and simple releases,
• require opam to be version 2.0.2 or later, allowing pin-depends in config.ml. pin-depends allows you to depend on a development branch of any opam package for your unikernel,
• adjusted documentation to adhere to odoc requirements,
• the mirage command-line utility now emits lower and upper bounds of opam packages, allowing uncompromising deprecation of packages,
• support for OCaml 4.06.0 (and above), where safe-string is enabled by default. Strings are immutable now!!,
• remove usage of result package, which has incorporated into Pervasives since OCaml 4.03.0.

The 3.5.0 release contains several API improvements of different MirageOS interfaces - if you're developing your own MirageOS unikernels, you may want to read this post to adjust to the new APIs.

MirageOS interface API changes:

• mirage-clock has the type t constrained to unit as of 2.0.0;
• mirage-protocols renames the ETHIF module type to the clearer ETHERNET. As of 2.0.0 it also contains keep-alive support, complies with recent TCP/IP layering rework (see below), and IPv4 now supports reassembly and fragmentation;
• mirage-net reflects revised layering API as of 2.0.0 (see below);
• mirage-kv has a revised API and introduction of a read-write key-value store (see below).

Major changes

Key-value store

We improved the key-value store API, and added a read-write store. There is also ongoing work which implements the read-write interface using irmin, a branchable persistent storage that can communicate via the git protocol. Motivations for these changes were the development of CalDAV, but also the development of wodan, a flash-friendly, safe and flexible filesystem. The goal is to EOL the mirage-fs interface in favour of the key-value store.

Major API improvements (in this PR, since 2.0.0):

• The key is now a path (list of segments) instead of a string
• The value type is now a string
• The new function list : t -> key -> (string * [Value|Dictionary], error) result io was added
• The function get : t -> key -> (value, error) result io is now provided (used to be named read and requiring an offset and length parameter)
• The functions last_modified : t -> key -> (int * int64, error) result io and digest : t -> key -> (string, error) result io have been introduced
• The function size was removed.
• The signature RW for read-write key-value stores extends RO with three functions set, remove, and batch

There is now a non-persistent in-memory implementation of a read-write key-value store available. Other implementations (such as crunch, mirage-kv-unix, mirage-fs, tar have been adapted, as well as clients of mirage-kv (dns, cohttp, tls)).

TCP/IP

The IPv4 implementation now has support for fragment reassembly. Each incoming IPv4 fragment is checked for the "more fragments" and "offset" fields. If these are non-zero, the fragment is processed by the fragment cache, which uses a least recently used data structure of maximum size 256kB content shared by all incoming fragments. If there is any overlap in fragments, the entire packet is dropped (avoiding security issues). Fragments may arrive out of order. The code is heavily unit-tested. Each IPv4 packet may at most be in 16 fragments (to minimise CPU DoS with lots of small fragments), the timeout between the first and last fragment is 10 seconds.

The layering and allocation discipline has been revised. ethernet (now encapsulating and decapsulating Ethernet) and arp (the address resolution protocol) are separate opam packages, and no longer part of tcpip.

At the lowest layer, mirage-net is the network device. This interface is implemented by our different backends (xen, solo5, unix, macos, and vnetif). Some backends require buffers to be page-aligned when they are passed to the host system. This was previously not really ensured: while the abstract type page_aligned_buffer was required, write (and writev) took the abstract buffer type (always constrained to Cstruct.t by mirage-net-lwt). The mtu (maximum transmission unit) used to be an optional connect argument to the Ethernet layer, but now it is a function which needs to be provided by mirage-net.

The Mirage_net.write function now has a signature that is explicit about ownership and lifetime: val write : t -> size:int -> (buffer -> int) -> (unit, error) result io. It requires a requested size argument to be passed, and a fill function which is called with an allocated buffer, that satisfies the backend demands. The fill function is supposed to write to the buffer, and return the length of the frame to be send out. It can neither error (who should handle such an error anyways?), nor is it in the IO monad. The fill function should not save any references to the buffer, since this is the network device's memory, and may be reused. The writev function has been removed.

The Ethernet layer does encapsulation and decapsulation now. Its write function has the following signature: val write: t -> ?src:macaddr -> macaddr -> Ethernet.proto -> ?size:int -> (buffer -> int) -> (unit, error) result io. It fills in the Ethernet header with the given source address (defaults to the device's own MAC address) and destination address, and Ethernet protocol. The size argument is optional, and defaults to the MTU. The buffer that is passed to the fill function is usable from offset 0 on. The Ethernet header is not visible at higher layers.

The IP layer also embeds a revised write signature: val write: t -> ?fragment:bool -> ?ttl:int -> ?src:ipaddr -> ipaddr -> Ip.proto -> ?size:int -> (buffer -> int) -> buffer list -> (unit, error) result io. This is similar to the Ethernet signature - it writes the IPv4 header and sends a packet. It also supports fragmentation (including setting the do-not-fragment bit for path MTU discovery) -- whenever the payload is too big for a single frame, it is sent as multiple fragmented IPv4 packets. Additionally, setting the time-to-live is now supported, meaning we now can implement traceroute! The API used to include two functions, allocate_frame and write, where only buffers allocated by the former should be used in the latter. This has been combined into a single function that takes a fill function and a list of payloads. This change is for maximum flexibility: a higher layer can either construct its header and payload, and pass it to write as payload argument (the buffer list), which is then copied into the buffer(s) allocated by the network device, or the upper layer can provide the callback fill function to assemble its data into the buffer allocated by the network device, to avoid copying. Of course, both can be used - the outgoing packet contains the IPv4 header, and possibly the buffer until the offset returned by fill, and afterwards the payload.

The TCP implementation has preliminary keepalive support.

Solo5

• MirageOS 3.0.0 used the 0.2.0 release of solo5
• The ukvm target was renamed to hvt, where solo5-hvt is the monitoring process
• Support for FreeBSD bhyve and OpenBSD VMM hypervisor (within the hvt target)
• Support for ARM64 and KVM
• New target muen.sk, a separation kernel developed in SPARK/Ada
• New target GenodeOS, an operating system framework using a microkernel
• Debugger support: attach gdb in the host system for improved debugging experience
• Core dump support
• Drop privileges on OpenBSD and FreeBSD
• Block device write fixes (in mirage-block-solo5)

random

The default random device from the OCaml standard library is now properly seeded using mirage-entropy. In the future, we plan to make the fortuna RNG the default random number generator.

Argument passing to unikernels

The semantics of arguments passed to a MirageOS unikernel used to vary between different backends, now they're the same everywhere: all arguments are concatenated using the whitespace character as separator, and split on the whitespace character again by parse-argv. To pass a whitespace character in an argument, the whitespace now needs to be escaped: --hello=foo\ bar.

Noteworthy package updates

• cstruct 3.6.0 API changes and repackaging, see this announcement and this announcement
• ipaddr 3.0.0 major API changes, the s-expression serialisation is a separate subpackage, macaddr is now a standalone opam package
• base64 3.0.0 performance and API changes, see this announcement
• git 2.0.0, read this announcement, as well as its design and implementation
• io-page 2.0.0, see this announcement
• cohttp 2.0.0, see this announcement
• dns 1.0.0, see this announcement
• conduit 1.0.0, see this announcement

More features and bugfixes

• More HTTP server choices are supported via a new httpaf device that permits the high performance httpaf stack to run as a unikernel now.
• libvirt.xml is generated for virtio target
• Unix target now include -tags thread (for mirage-framebuffer SDL support)
• Various modules (IPv6, DHCP) are explicit about their dependency to the random device
• QubesDB can be requested in config.ml when the target is Xen

You may also want to read the MirageOS 3.2.0 announcement and the MirageOS 3.3.0 announcement.

Next steps

We are working on further changes which revise the mirage internal build system to dune. At the moment it uses ocamlbuild, ocamlfind, pkg-config, and make. The goal of this change is to make MirageOS more developer-friendly. On the horizon we have MirageOS unikernel monorepos, incremental builds, pain-free cross-compilation, documentation generation, ...

Several other MirageOS ecosystem improvements are on the schedule for 2019, including an irmin 2.0 release, a seccomp target for Solo5, and easier deployment and multiple interface in Solo5.

We are pleased to announce the first release of Techelson, available here.

Techelson is a Test Execution Engine for Michelson. It aims at testing functional properties of Michelson smart contracts. Make sure to check the user documentation to get a sense of Techelson’s workflow and features.

For Liquidity programmers interested in Techelson, take a look at this blog post discussing how to write tests in Liquidity and run them using Techelson.

Techelson is still young: if you have problems…

We are pleased to announce the first release of Techelson, available here.

Techelson is a Test Execution Engine for Michelson. It aims at testing functional properties of Michelson smart contracts. Make sure to check the user documentation to get a sense of Techelson’s workflow and features.

For Liquidity programmers interested in Techelson, take a look at this blog post discussing how to write tests in Liquidity and run them using Techelson.

Techelson is still young: if you have problems, suggestions or feature requests please open an issue on the repository.

Smart contracts calls already provide a built-in authentication mechanism as transactions (i.e. call operations) are cryptographically signed by the sender of the transaction. This is a guarantee on which programs can rely.

However, sometimes you may want more involved or flexible authentication schemes. The ones that rely on signature validity checking can be implemented in Michelson, and Liquidity provide a built-in instruction to do so. (You still need to keep in mind that you cannot store un…

Smart contracts calls already provide a built-in authentication mechanism as transactions (i.e. call operations) are cryptographically signed by the sender of the transaction. This is a guarantee on which programs can rely.

However, sometimes you may want more involved or flexible authentication schemes. The ones that rely on signature validity checking can be implemented in Michelson, and Liquidity provide a built-in instruction to do so. (You still need to keep in mind that you cannot store unencrypted confidential information on the blockchain).

This instruction is Crypto.check in Liquidity. Its type can be written as:

Crypto.check: key -> signature -> bytes -> bool

Which means that it takes as arguments a public key, a signature and a sequence of bytes and returns a Boolean. Crypto.check pub_key signature message is true if and only if the signature signature was obtained by signing the Blake2b hash of message using the private key corresponding to the public key pub_key.

A small smart contract snippet which implements a signature check (against a predefined public key kept in the smart contract’s storage) can be tested online here.

type storage = key

let%entry main ((message : string), (signature : signature)) key =
  let bytes = Bytes.pack message in
  if not (Crypto.check key signature bytes) then
    failwith "Wrong signature";
  ([] : operation list), key

This smart contract fails if the string message was not signed with the private key corresponding to the public key key stored. Otherwise it does nothing.

This signature scheme is more flexible than the default transaction/sender one, however it requires that the signature can be built outside of the smart contract. (And more generally outside of the toolset provided by Liquidity and Tezos). On the other hand, signing a transaction is something you get for free if you use the tezos client or any tezos wallet (as is it essentially their base function).

The rest of this blog post will focus on various ways to sign data, and on getting signatures that can be used in Tezos and Liquidity directly.

Signing Using the Tezos Client

One (straightforward) way to sign data is to use the Tezos client directly. You will need to be connected to a Tezos node though as the client makes RPCs to serialize data (this operation is protocol dependent). We can only sign sequences of bytes, so the first thing we need to do is to serialize whichever data we want to sign. This can be done with the command hash data of the client.

> ./tezos-client -A alphanet-node.tzscan.io -P 80 hash data '"message"' of type string
Raw packed data: 0x0501000000076d657373616765
Hash: exprtXaZciTDGatZkoFEjE1GWPqbJ7FtqAWmmH36doxBreKr6ADcYs
Raw Blake2b hash: 0x01978930fd2d04d0db8c2e4ef8a3f5d63b8e732177c8723135ed0dc7d99ebed3
Raw Sha256 hash: 0x32569319f6517036949bcead23a761bfbfcbf4277b010355884a86ba09349839
Raw Sha512 hash: 0xdfa4ea9f77db3a98654f101be1d33d56898df40acf7c2950ca6f742140668a67fefbefb22b592344922e1f66c381fa2bec48aa47970025c7e61e35d939ae3ca0
Gas remaining: 399918 units remaining

This command gives the result of hashing the data using various algorithms but what we’re really interested in is the first item Raw packed data which is the serialized version of our data ("message") : 0x0501000000076d657373616765.

We can now sign these bytes using the Tezos client as well. This step can be performed completely offline, for that we need to use the option -p of the client to specify the protocol we want to use (the sign bytes command will not be available without first selecting a valid protocol). Here we use protocol 3, designated by its hash PsddFKi3.

> ./tezos-client -p PsddFKi3 sign bytes 0x0501000000076d657373616765 for my_account
Signature: edsigto9QHtXMyxFPyvaffRfFCrifkw2n5ZWqMxhGRzieksTo8AQAFgUjx7WRwqGPh4rXTBGGLpdmhskAaEauMrtM82T3tuxoi8

The account my_account can be any imported account in the Tezos client. In particular, it can be an encrypted key pair (you will need to enter a password to sign) or a hardware Ledger (you will need to confirm the signature on the Ledger). The obtained signature can be used as is with Liquidity or Michelson. This one starts with edsig because it was obtained using an Ed25519 private key, but you can also get signatures starting with spsig1 or p2sig depending on the cryptographic curve that you use.

Signing Manually

In this second section we detail the necessary steps and provide a Python script to sign string messages using an Ed25519 private key. This can be easily adapted for other signing schemes.

These are the steps that will need to be performed in order to sign a string:

1. Assuming that the value you want to sign is a string, you first need to convert its ASCII version to hexa, for the string "message" that is 6d657373616765.
2. You need to produce the packed version of the corresponding Michelson expression. The binary representation can vary depending on the types of the values you want to pack but for strings it is:

   | 0x | 0501 | [size of the string on 4 bytes] | [ascii string in hexa] |

   for "message" (of length 7), it is

   | 0x | 0501 | 00000007 | 6d657373616765 |

   or 0x0501000000076d657373616765.

3. Hash this value using Blake2b (01978930fd2d04d0db8c2e4ef8a3f5d63b8e732177c8723135ed0dc7d99ebed3) which is 32 bytes long.
4. Depending on your public key, you then need to sign it with the corresponding curve (ed25519 for edpk keys), the signature is 64 bytes:

   753e013b8515a7d47eaa5424de5efa2f56620ac8be29d08a6952ae414256eac44b8db71f74600275662c8b0c226f3280e9d24e70a5fa83015636b98059b5180c

5. Optionally convert to base58check. This is not needed because Liquidity and Michelson allow signatures (as well as keys and key hashes) to be given in hex format with a 0x:

   0x753e013b8515a7d47eaa5424de5efa2f56620ac8be29d08a6952ae414256eac44b8db71f74600275662c8b0c226f3280e9d24e70a5fa83015636b98059b5180c

The following Python (3) script will do exactly this, entirely offline. Note that this is just an toy example, and should not be used in production. In particular you need to give your private key on the command line so this might not be secure if the machine you run this on is not secure.

> pip3 install base58check pyblake2 ed25519
> python3 ./sign_string.py "message" edsk2gL9deG8idefWJJWNNtKXeszWR4FrEdNFM5622t1PkzH66oH3r
0x753e013b8515a7d47eaa5424de5efa2f56620ac8be29d08a6952ae414256eac44b8db71f74600275662c8b0c226f3280e9d24e70a5fa83015636b98059b5180c

sign_string.py

from pyblake2 import blake2b
import base58check
import ed25519
import sys

message = sys.argv[1]
seed_b58 = sys.argv[2]

prefix = b'\x05\x01'
len_bytes = (len(message)).to_bytes(4, byteorder='big')
h = blake2b(digest_size=32)
b = bytearray()
b.extend(message.encode())
h.update(prefix + len_bytes + b)
digest = h.digest()

seed = base58check.b58decode(seed_b58)[4:-4]
sk = ed25519.SigningKey(seed)
sig = sk.sign(digest)
print("0x" + sig.hex())

As part of my PhD at Gallium, I have been working on formally proving OCaml programs using Coq. More precisely, the focus has been on proving not only that a program is functionally correct (always compute the right result), but also does so in the expected amount of time. In other words, we are interested in formally verifying the asymptotic complexity of OCaml programs.

In this blog-post, I’m happy to report on our latest endeavour: the verification of the correctness and (amortized) compl…

As part of my PhD at Gallium, I have been working on formally proving OCaml programs using Coq. More precisely, the focus has been on proving not only that a program is functionally correct (always compute the right result), but also does so in the expected amount of time. In other words, we are interested in formally verifying the asymptotic complexity of OCaml programs.

In this blog-post, I’m happy to report on our latest endeavour: the verification of the correctness and (amortized) complexity of a state-of-the art incremental cycle detection algorithm.

This is joint work with Jacques-Henri Jourdan and my advisors François Pottier and Arthur Charguéraud.

The initial motivation for this work comes from the implementation of Coq itself! More specifically, efficiently checking the consistency of universe constraints that result from the type-checking phase is a difficult problem, that can be seen as an incremental cycle detection problem. A few years ago, Jacques-Henri reimplemented the part of Coq responsible for this, following a state-of-the-art algorithm published by Bender, Fineman, Gilbert and Tarjan. They prove that using their algorithm, adding an edge in a graph with m edges and n nodes while ensuring that after each addition the graph remains acyclic has amortized asymptotic complexity O(min (m^1/2, n^2/3)). In the common case where the graph is sparse enough, this is equivalent to O(√m).

Jacques-Henri’s implementation resulted in a nice speedup in practice, but it is not so easy to convince oneself that it indeed has the right asymptotic complexity in all cases (in other words, that it does not have a “complexity bug”). The amortized analysis required to establish the O() bound on paper is quite subtle, and for instance relies on a parameter Δ computed at runtime that looks quite magical at first glance.

In the work I’m presenting here, we try to untangle this mystery. We give a formally verified OCaml implemention for a (slightly modified) incremental cycle detection algorithm from Bender et al. We prove that it is not only correct, but also satisfies the expected complexity bound.

Note that this is not yet the exact algorithm that is currently part of Coq’s implementation, but still an important milestone on the way there! (Coq implements the variant by Bender et al. that additionally maintains “strong components”. We believe it could be implemented and verified in a modular fashion, by combining the algorithm we present here and a union-find data structure.)

Here’s the draft (currently under submission), and a link to the OCaml code and Coq proofs:

http://gallium.inria.fr/~fpottier/publis/gueneau-jourdan-chargueraud-pottier-2019.pdf

https://gitlab.inria.fr/agueneau/incremental-cycles

We exploit Separation Logic with Time Credits to verify the correctness and worst-case amortized asymptotic complexity of a state-of-the-art incremental cycle detection algorithm.

Happy reading!

After the hard work done on the integration of floating-point arithmetic reasoning two years ago, 2018 is the year of polymorphic SMT2 support and efficient SAT solving for Alt-Ergo. In this post, we recap the main novelties last year, and we announce the first Alt-Ergo Users’ Club meeting.

An SMT2 front-end with prenex polymorphism

As you may know, Alt-Ergo’s native input language is not compliant with the SMT-LIB 2 input language standard, and translating formulas from SMT-LIB 2 to…

After the hard work done on the integration of floating-point arithmetic reasoning two years ago, 2018 is the year of polymorphic SMT2 support and efficient SAT solving for Alt-Ergo. In this post, we recap the main novelties last year, and we announce the first Alt-Ergo Users’ Club meeting.

An SMT2 front-end with prenex polymorphism

As you may know, Alt-Ergo’s native input language is not compliant with the SMT-LIB 2 input language standard, and translating formulas from SMT-LIB 2 to Alt-Ergo’ syntax (or vice-versa) is not immediate. Besides its extension with polymorphism, this native language diverges from SMT-LIB’s by distinguishing terms of type boolean from formulas (that are propositions). This distinction makes it hard, for instance, to efficiently translate let-in and if-then-else constructs that are ubiquitous in SMT-LIB 2 benchmarks.

In order to work closely with the SMT community, we designed a conservative extension of the SMT-LIB 2 standard with prenex polymorphism and implemented it as a new frontend in Alt-Ergo 2.2. This work has been published in the 2018 edition of the SMT-Workshop. An online version of the paper is available here. Experimental results showed that polymorphism is really important for Alt-Ergo, as it allows to improve both resolution rate and resolution time (see Figure 5 in the paper for more details).

Improved SAT solvers

We also worked on improving SAT-solving in Alt-Ergo last year. The main direction towards this goal was to extend our CDCL-based SAT solver to mimic some desired behaviors of the native Tableaux-like SAT engine. Generally speaking, this allows a better management of the context during proof search, which prevents from overwhelming theories and instantiation engines with useless facts. A comparison of this solver with Alt-Ergo’s old Tableaux-like solver is also done in our SMT-Workshop paper.

SMT-Comp and SMT-Workshop 2018

As emphasized above, we published our work regarding polymorphic SMT2 and SAT solving in SMT-Workshop 2018. More generally, this was an occasion for us to write the first tool paper about Alt-Ergo, and to highlight the main features that make it different from other state-of-the-art SMT solvers like CVC4, Z3 or Yices.

Thanks to our new SMT2 frontend, we were able to participate to the SMT-Competition last year. Naturally, we selected categories that are close to “deductive program verification”, as Alt-Ergo is primarily tuned for formulas coming from this application domain.

Although Alt-Ergo did not rank first, it was a positive experience and this encourages us to go ahead. Note that Alt-Ergo’s brother, Ctrl-Ergo, was not far from winning the QF-LIA category of the competition. This performance is partly due to the improvements in the CDCL SAT solver that were also integrated in Ctrl-Ergo.

Alt-Ergo for Atelier-B

Atelier-B is a framework that allows to develop formally verified software using the B Method. The framework rests on an automatic reasoner that allows to discharges thousands of mathematical formulas extracted from B models. If a formula is not discharged automatically, it is proved interactively. ClearSy (the company behind development of Atelier-B) has recently added a new backend to produce verification conditions in Why3’s logic, in order to target more automatic provers and increase automation rate. For certifiability reasons, we extended Alt-Ergo with a new frontend that is able to directly parse these verification conditions without relying on Why3.

Improved hash-consed data-structures

As said above, Alt-Ergo makes a clear distinction between Boolean terms and Propositions. This distinction prevents us from doing some rewriting and simplifications, in particular on expressions involving let-in and if-then-else constructs. This is why we decided to merge Term, Literal, and Formula in a new Expr data-structure, and remove this distinction. This allowed us to implement some additional simplification steps, and we immediately noticed performance improvements, in particular on SMT2 benchmarks. For instance, Alt-Ergo 2.3 proves 19548 formulas of AUFLIRA category in ~350 minutes, while version 2.2 proves 19535 formulas in ~1450 minutes (time limit was set to 20 minutes per formula).

Towards the integration of algebraic datatypes

Last Autumn, we also started working on the integration of algebraic datatypes reasoning in Alt-Ergo. In this first iteration, we extended Alt-Ergo’s native language to be able to declare (mutually recursive) algebraic datatypes, to write expressions with patterns matching, to handle selectors, … We then extended the typechecker accordingly and implemented a (not that) basic theory reasoner. Of course, we also handle SMT2’s algebraic datatypes. Here is an example in Alt-Ergo’s native syntax:

type ('a, 'b) t = A of {a_1 : 'a} | B of {b_11 : 'a ; b12 : 'b} | C | D | E

logic e : (int, real) t
logic n : int

axiom ax_n : n >= 9

axiom ax_e:
  e = A(n) or e = B(n*n, 0.) or e = E

goal g:
  match e with
   | A(u) -> u >= 8
   | B (u,v) -> u >= 80 and v = 0.
   | E -> true
   | _ -> false
  end 
  and 3 <= 2+2

What is planned in 2019 and beyond: the Alt-Ergo’s Users’ Club is born!

In 2018, we welcomed a lot of new engineers with a background in formal methods: Steven (De Oliveira) holds a PhD in formal verification from the Paris-Saclay University and the French Atomic Energy Commission (CEA). He has a master in cryptography and worked in the Frama-C team, developing open-source tools for verifying C programs. David (Declerck) obtained a PhD from Université Paris-Saclay in 2018, during which he extended the Cubicle model checker to support weak memory models and wrote a compiler from a subset of the x86 assembly language to Cubicle. Guillaume (Bury) holds a PhD from Université Sorbonne Paris Cité. He studied the integration of rewriting techniques inside SMT solvers. Albin (Coquereau) is working as a PhD student between OCamlPro, LRI and ENSTA, focusing on improving the Alt-Ergo SMT solver. Adrien is interested in verification of safety properties over software and embedded systems. He worked on higher-order functional program verification at the University of Tokyo, and on the Kind 2 model checker at the University of Iowa. All these people will consolidate the department of formal methods at OCamlPro, which will be beneficial for Alt-Ergo.

In 2019 we just launched the Alt-Ergo Users’ Club, in order to get closer to our users, collect their needs, and integrate them into the Alt-Ergo roadmap, but also to ensure sustainable funding for the development of the project. We are happy to announce the very first member of the Club is Adacore, very soon to be followed by Trust-In-Soft and CEA List. Thanks for your early support!

Interested to join? Contact us: contact@ocamlpro.com

 

Generally, every program I write, regardless of what useful thing it actually does, and regardless of what programming language it is written in, has to do certain things, which usually includes

• Importing a library and calling functions contained within that library
• Handling datatypes such as converting between strings and integers, and knowing when this is implicit or explicit, how dates and times work, and so on
• Getting command line parameters or parsing a configuration file
• Writing log messa…

Generally, every program I write, regardless of what useful thing it actually does, and regardless of what programming language it is written in, has to do certain things, which usually includes

• Importing a library and calling functions contained within that library
• Handling datatypes such as converting between strings and integers, and knowing when this is implicit or explicit, how dates and times work, and so on
• Getting command line parameters or parsing a configuration file
• Writing log messages such as to files or the system log
• Handling errors and exceptions
• Connecting to services such as a database, a REST API, a message bus etc
• Reading and writing files to the disk, or to blob storage or whatever it’s called this week
• Spawning threads and processes and communicating between them
• Building a package whether that’s a self-contained binary, an RPM, an OCI container, whatever is native to that language and the platform

It’s easy to find examples of most of these things using resources such as Rosetta Code and my first real program will be a horrific cut and paste mess – but it will get me started and I’ll soon refine it and absorb the idiomatic patterns of the language and soon be writing fluently in it, and knowing my way around the ecosystem, what libraries are available, which are the strengths and weaknesses of the language, the libraries, the community and so on. Once you have done this a few times it becomes easy and you can stop worrying so much about being a “language X programmer” and concentrate on the important stuff, which is the problem domain you are working in.

MirageOS is a library operating system written from the ground up in OCaml. It has an impossible and incredibly huge goal to re-implement all of the world! Looking back at the work accomplished by the MirageOS team, it appears that's what happened for several years. Re-implementing the entire stack, in particular the lower layers that we often take for granted, requires a great attention to detail. While it may seem reasonably easy to implement a given RFC, a huge amount of work is often hid…

MirageOS is a library operating system written from the ground up in OCaml. It has an impossible and incredibly huge goal to re-implement all of the world! Looking back at the work accomplished by the MirageOS team, it appears that's what happened for several years. Re-implementing the entire stack, in particular the lower layers that we often take for granted, requires a great attention to detail. While it may seem reasonably easy to implement a given RFC, a huge amount of work is often hidden under the surface.

In this article, we will explain the development process we went through, as we updated a small part of the MirageOS stack: the library ocaml-base64. It's a suitable example as the library is small (few hundreds lines of code), but it needs ongoing development to ensure good quality and to be able to trust it for higher level libraries (like mrmime).

Updating the library was instigated by a problem I ran into with the existing base64 implementation while working on the e-mail stack. Indeed, we got some errors when we tried to compute an encoded-word according to the RFC 2047. So after several years of not being touched, we decided to update `ocaml-base64`.

The Critique of Pure Reason

The first problem

We started by attempting to use ocaml-base64 on some examples extracted from actual e-mails, and we quickly ran into cases where the library failed. This highlighted that reality is much more complex than you can imagine from reading an RFC. In this situation, what do you do: try to implement a best-effort strategy and continue parsing? Or stick to the letter of the RFC and fail? In the context of e-mails, which has accumulated a lot of baggage over time, you cannot get around implementing a best-effort strategy.

The particular error we were seeing was a Not_found exception when decoding an encoded-word. This exception appeared because the implementation relied on String.contains, and the input contained a character which was not part of the base64 alphabet.

This was the first reason why we thought it necessary to rewrite ocaml-base64. Of course, we could just catch the exception and continue the initial computation, but then another reason appeared.

The second problem

As @clecat and I reviewed RFC 2045, we noticed the following requirement:

The encoded output stream must be represented in lines of no more than 76 characters each.

See RFC 2045, section 6.8

Pretty specific, but general to e-mails, we should never have more than 78 characters per line according to RFC 822, nor more than 998 characters according to RFC 2822.

Having a decoder that abided RFC 2045 more closely, including the requirement above, further spurred us to implement a new decoder.

As part of the new implementation, we decided to implement tests and fuzzers to ensure correctness. This also had the benefit, that we could run the fuzzer on the existing codebase. When fuzzing an encoder/decoder pair, an excellent check is whether the following isomorphism holds:

let iso0 input = assert (decode (encode input) = input)
let iso1 input = assert (encode (decode input) = input)

However, at this point @hannesm ran into another error (see #20).

The third problem

We started to review the `nocrypto` implementation of base64, which respects our requirements. We had some concerns about the performance of the implementation though, so we decided to see if we would get a performance regression by switching to this implementation.

A quick benchmark based on random input revealed the opposite, however! nocrypto's implementation was faster than ocaml-base64:

ocaml-base64's implementation on bytes (length: 5000): 466 272.34ns
nocrypto's implementation on bytes (length: 5000): 137 406.04ns

Based on all these observations, we thought there was sufficient reason to reconsider the ocaml-base64 implementation. It's also worth mentioning that the last real release (excluding dune/jbuilder/topkg updates) is from Dec. 24 2014. So, it's pretty old code and the OCaml eco-system has improved a lot since 2014.

Implementation & review

We started integrating the nocrypto implementation. Of course, implementing RFC 4648 is not as easy as just reading examples and trying to do something which works. The devil is in the detail.

@hannesm and @cfcs decided to do a big review of expected behavior according to the RFC, and another about implementation and security issues.

Canonicalization

The biggest problem about RFC 4648 is regarding canonical inputs. Indeed, there are cases where two different inputs are associated with the same value:

let a = Base64.decode "Zm9vCg==" ;;
- : string = "foo\n"
let b = Base64.decode "Zm9vCh==" ;;
- : string = "foo\n"

This is mostly because the base64 format encodes the input 6 bits at a time. The result is that 4 base64 encoded bytes are equal to 3 decoded bytes (6 * 4 = 8 * 3). Because of this, 2 base64 encoded bytes provide 1 byte plus 4 bits. What do we need to do with these 4 bits? Nothing.

That's why the last character in our example can be something else than g. g is the canonical byte to indicate using the 2 bits afterward the 6 bits delivered by C (and make a byte - 8 bits). But h can be used where we just need 2 bits at the end.

Due to this behavior, the check used for fuzzing changes: from a canonical input, we should check isomorphism.

Invalid character

As mentioned above ("The first problem"), how should invalid characters be handled? This happens when decoding a byte which is not a part of the base64 alphabet. In the old version, ocaml-base64 would simply leak a Not_found exception from String.contains.

The MirageOS team has taken a stance on exceptions, which is to "use exceptions for exceptional conditions" - invalid input is hardly one of those. This is to avoid any exception leaks, as it can be really hard to track the origin of an exception in a unikernel. Because of this, several packages have been updated to return a result type instead, and we wanted the new implementation to follow suit.

On the other hand, exceptions can be useful when considered as a more constrained form of assembly jump. Of course, they break the control flow, but from a performance point of view, it's interesting to use this trick:

exception Found

let contains str chr =
  let idx = ref 0 in
  let len = String.length str in
  try while !idx < len
      do if String.unsafe_get str !idx = chr then raise Found ; incr idx done ;
      None
  with Found -> Some !idx

This kind of code for example is ~20% faster than String.contains.

As such, exceptions can be a useful tool for performance optimizations, but we need to be extra careful not to expose them to the users of the library. This code needs to be hidden behind a fancy functional interface. With this in mind, we should assert that our decode function never leaks an exception. We'll describe how we've adressed this problem later.

Special cases

RFC 4648 has some detailed cases and while we would sometimes like to work in a perfect world where we will never need to deal with such errors, from our experience, we cannot imagine what the end-user will do to formats, protocols and such.

Even though the RFC has detailed examples, we have to read between lines to know special cases and how to deal with them.

@hannesm noticed one of these cases, where padding (= sign at the end of input) is not mandatory:

The pad character "=" is typically percent-encoded when used in an URI [9], but if the data length is known implicitly, this can be avoided by skipping the padding; see section 3.2.

See RFC 4648, section 5

That mostly means that the following kind of input can be valid:

let a = Base64.decode ~pad:false "Zm9vCg"
- : string = "foo\n"

It's only valid in a specific context though: when length is known implicitly. Only the caller of decode can determine whether the length is implicitly known such that padding can be omitted. To that end, we've added a new optional argument ?pad to the function Base64.decode.

Allocation, sub, ?off and ?len

Xavier Leroy has described the garbage collector in the following way:

You see, the Caml garbage collector is like a god from ancient mythology: mighty, but very irritable. If you mess with it, it'll make you suffer in surprising ways.

That's probably why my experience with improving the allocation policy of (ocaml-git)ocaml-git was quite a nightmare. Allowing the user to control allocation is important for efficiency, and we wanted to ocaml-base64 to be a good citizen.

At the beginning, ocaml-base64 had a very simple API:

val decode : string -> string
val encode : string -> string

This API forces allocations in two ways.

Firstly, if the caller needs to encode a part of a string, this part needs to be extracted, e.g. using String.sub, which will allocate a new string. To avoid this, two new optional arguments have been added to encode: ?off and ?len, which specifies the substring to encode. Here's an example:

(* We want to encode the part 'foo' without prefix or suffix *)

(* Old API -- forces allocation *)
Base64.encode (String.sub "prefix foo suffix" 7 3) ;;
- : string = "Zm9v"

(* New API -- avoids allocation *)
Base64.encode ~off:7 ~len:3 "prefix foo suffix" ;;
- : string = "Zm9v"

Secondly, a new string is allocated to hold the resulting string. We can calculate a bound on the length of this string in the following manner:

let (//) x y =
  if y < 1 then raise Division_by_zero ;
  if x > 0 then 1 + ((x - 1) / y) else 0

let encode input =
  let res = Bytes.create (String.length input // 3 * 4) in
  ...

let decode input =
  let res = Bytes.create (String.length input // 4 * 3) in
  ...

Unfortunately we cannot know the exact length of the result prior to computing it. This forces a call to String.sub at the end of the computation to return a string of the correct length. This means we have two allocations rather than one. To avoid the additional allocation, [@avsm][avsm] proposed to provide a new type sub = string * int * int. This lets the user call String.sub if required (and allocate a new string), or use simply use the returned sub for _blit_ting to another buffer or similar.

Fuzz everything!

There's a strong trend of fuzzing libraries for MirageOS, which is quite easy thanks to the brilliant work by @yomimono and @stedolan! The integrated fuzzing in OCaml builds on American fuzzy lop, which is very smart about discarding paths of execution that have already been tested and generating unseen inputs which break your assumptions. My first experience with fuzzing was with the library `decompress`, and I was impressed by precise error it found about a name clash.

Earlier in this article, I listed some properties we wanted to check for ocaml-base64:

• The functions encode and decode should be be isomorphic taking canonicalization into account:

let iso0 input =
  match Base64.decode ~pad:false input with
  | Error _ -> fail ()
  | Ok result0 ->
    let result1 = Base64.encode_exn result0 in
    match Base64.decode ~pad:true result1 with
    | Error _ -> fail ()
    | Ok result2 -> check_eq result0 result2

let iso1 input =
  let result = Base64.encode_exn input in
  match Base64.decode ~pad:true result0 with
  | Error _ -> fail ()
  | Ok result1 ->
    let result2 = Base64.encode_exn result1 in
    check_eq result0 result2

• The function decode should never raise an exception, but rather return a result type:

let no_exn input =
  try ignore @@ Base64.decode input with _ -> fail ()

• And finally, we should randomize ?off and ?len arguments to ensure that we don't get an Out_of_bounds exception when accessing input.

Just because we've applied fuzzing to the new implementation for a long time, it doesn't mean that the code is completely infallible. People can use our library in an unimaginable way (and it's mostly what happens in the real world) and get an unknowable error.

But, with the fuzzer, we've managed to test some properties across a very wide range of input instead of unit testing with random (or not so random) inputs from our brains. This development process allows fixing the semantics of implementations (even if it's not a formal definition of semantics), but it's better than nothing or outdated documentation.

Conclusion

Based on our recent update to ocaml-base64, this blog post explains our development process as go about rewriting the world to MirageOS, one bit at a time. There's an important point to be made though:

ocaml-base64 is a small project. Currently, the implementation is about 250 lines of code. So it's a really small project. But as stated in the introduction, we are fortunate enough to push the restart button of the computer world - yes, we want to make a new operating system.

That's a massive task, and we shouldn't make it any harder on ourselves than necessary. As such, we need to justify any step, any line of code, and why we decided to spend our time on any change (why we decided to re-implement git for example). So before committing any time to projects, we try to do a deep analysis of the problem, get feedback from others, and find a consensus between what we already know, what we want and what we should have (in the case of ocaml-base64, @hannesm did a look on the PHP implementation and the Go implementation).

Indeed, this is a hard question which nobody can answer perfectly in isolation. So, the story of this update to ocaml-base64 is an invitation for you to enter the arcanas of the computer world through MirageOS :) ! Don't be afraid!

This article is the third post of a series of posts on improving Tezos storage.  In our previous post, we announced the availability of a docker image for beta testers, wanting to test our storage and garbage collector. Today, we are glad to announce that we rebased our code on the latest version of mainnet-staging, and pushed a branch mainnet-staging-irontez on our public Gitlab repository:

https://gitlab.com/tzscan/tezos/commits/mainnet-staging-irontez

The only difference with the previous po…

This article is the third post of a series of posts on improving Tezos storage.  In our previous post, we announced the availability of a docker image for beta testers, wanting to test our storage and garbage collector. Today, we are glad to announce that we rebased our code on the latest version of mainnet-staging, and pushed a branch mainnet-staging-irontez on our public Gitlab repository:

https://gitlab.com/tzscan/tezos/commits/mainnet-staging-irontez

The only difference with the previous post is a change in the name of the RPCs : /storage/context/gc will trigger a garbage collection (and terminate the node afterwards) and /storage/context/revert will migrate the database back to Irmin (and terminate the node afterwards).

Enjoy and send us feedback !!

In a previous post, we presented some work that we did to improve the quantity of storage used by the Tezos node. Our post generated a lot of comments, in which upcoming features such as garbage collection and pruning were introduced. It also motivated us to keep working on this (hot) topic, and we present here our new results, and current state. Irontez3 is a new version of our storage system, that we tested both on real traces and real nodes. We implemented a garbage-collector for it, that is …

In a previous post, we presented some work that we did to improve the quantity of storage used by the Tezos node. Our post generated a lot of comments, in which upcoming features such as garbage collection and pruning were introduced. It also motivated us to keep working on this (hot) topic, and we present here our new results, and current state. Irontez3 is a new version of our storage system, that we tested both on real traces and real nodes. We implemented a garbage-collector for it, that is triggered by an RPC on our node (we want the user to be able to choose when it happens, especially for bakers who might risk losing a baking slot), and automatically every 16 cycles in our traces.

In the following graph, we present the size of the context database during a full trace execution (~278 000 blocks):

There is definitely quite some improvement brought to the current Tezos implementation based on Irmin+LMDB, that we reimplemented as IronTez0. IronTez0 allows an IronTez node to read a database generated by the current Tezos and switch to the IronTez3 database. At the bottom of the graph, IronTez3 increases very slowly (about 7 GB at the end), and the garbage-collector makes it even less expensive (about 2-3 GB at the end). Finally, we executed a trace where we switched from IronTez0 to IronTez3 at block 225 000. The graph shows that, after the switch, the size immediately grows much more slowly, and finally, after a garbage collection, the storage is reduced to what it would have been with IronTez3.

Now, let’s compare the speed of the different storages:

The graph shows that IronTez3 is about 4-5 times faster than Tezos/IronTez0. Garbage-collections have an obvious impact on the speed, but clearly negligible compared to the current performance of Tezos. On our computer used for the traces, a Xeon with an SSD disk, the longest garbage collection takes between 1 and 2 minutes, even when the database was about 40 GB at the beginning.

In the former post, we didn’t check the amount of memory used by our storage system. It might be expected that the performance improvement could be associated with a more costly use of memory… but such is not the case :

At the top of the graph is our IronTez0 implementation of the current storage: it uses a little more memory than the current Tezos implementation (about 6 GB), maybe because it shares data structures with IronTez3, with fields that are only used by IronTez3 and could be removed in a specialized version. IronTez3 and IronTez3 with garbage collection are at the bottom, using about 2 GB of memory. It is actually surprising that the cost of garbage collections is very limited.

On our current running node, we get the following storage:

$ du

1.4G ./context
4.9G ./store
6.3G .

Now, if we use our new RPC to revert the node to Irmin (taking a little less than 8 minutes on our computer), we get :

$ du
14.3G ./context
 4.9G ./store
19.2G .

Beta-Testing with Docker

If you are interested in these results, it is now possible to test our node: we created a docker image, similar to the ones of Tezos. It is available on Docker Hub (one image that works for both Mainnet and Alphanet). Our script mainnet.sh (http://tzscan.io/irontez/mainnet.sh) can be used similarly to the alphanet.sh script of Tezos to manage the container. It can be run on an existing Tezos database, it will switch it to IronTez3. Note that such a change is not irreversible, still it might be a good idea to backup your Tezos node directory before, as (1) migrating back might take some time, (2) this is a beta-testing phase, meaning the code might still hide nasty bugs, and (3) the official node might introduce a new incompatible format.

New RPCS

Both of these RPCs will make the node TERMINATE once they have completed. You should restart the node afterwards.

• The RPC /ocp/storage/gc : it triggers a garbage collection using the RPC /ocp/storage/gc . By default, this RPC will keep only the contexts from the last 9 cycles. It is possible to change this value by using the ?keep argument, and specify another number of contexts to keep (beware that if this value is too low, you might end up with a non-working Tezos node, so we have set a minimum value of 100). No garbage-collection will happen if the oldest context to keep was stored in the Irmin database.
• The RPC /ocp/storage/revert : it triggers a migration of the database fron Irontez3 back to Irmin. If you have been using IronTez for a while, and want to go back to the official node, this is the way. After calling this RPC, you should not run IronTez again, otherwise, it will restart using the IronTez3 format, and you will need to revert again. This operation can take a lot of time, depending on the quantity of data to move between the two formats.

Following Steps

We are now working with the team at Nomadic Labs to include our work in the public Tezos code base.  We will inform you as soon as our Pull Request is ready, for more testing ! If all testing and review goes well, we hope it can be merged in the next release !

A reflection on the new year… Today, Tezos is a global network and an open source project with developers spanning over five continents. In the inception of this project, the French company OCamlPro which, to this day, stills develops numerous projects around Tezos, played a particularly important role. Indeed, they were the first home of the research engineers who laid down the cornerstone of the code base, in tight collaboration with Arthur Breitman and the architect of the project, and …

A reflection on the new year… Today, Tezos is a global network and an open source project with developers spanning over five continents. In the inception of this project, the French company OCamlPro which, to this day, stills develops numerous projects around Tezos, played a particularly important role. Indeed, they were the first home of the research engineers who laid down the cornerstone of the code base, in tight collaboration with Arthur Breitman and the architect of the project, and DLS. We take some time today to remember those early days and celebrate the flourishing of this once small project.

Arthur and OCamlPro

(cross-post with Arthur Breitman, Founder of the Tezos project)

We are pleased to announce the release of opam 2.0.3.

This new version contains some backported fixes:

• Fix manpage remaining $ (OPAMBESTEFFORT)
• Fix OPAMROOTISOK handling
• Regenerate missing environment file

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 san…

We are pleased to announce the release of opam 2.0.3.

This new version contains some backported fixes:

• Fix manpage remaining $ (OPAMBESTEFFORT)
• Fix OPAMROOTISOK handling
• Regenerate missing environment file

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 major version, and remain open to bug reports and suggestions.

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

Running a Tezos node currently costs a lot of disk space, about 59 GB for the context database, the place where the node stores the states corresponding to every block in the blockchain, since the first one. Of course, this is going to decrease once garbage collection is integrated, i.e. removing very old information, that is not used and cannot change anymore (PR720 by Thomas Gazagnaire, Tarides, some early tests show a decrease to 14GB ,but with no performance evaluation). As a side note, thi…

Running a Tezos node currently costs a lot of disk space, about 59 GB for the context database, the place where the node stores the states corresponding to every block in the blockchain, since the first one. Of course, this is going to decrease once garbage collection is integrated, i.e. removing very old information, that is not used and cannot change anymore (PR720 by Thomas Gazagnaire, Tarides, some early tests show a decrease to 14GB ,but with no performance evaluation). As a side note, this is different from pruning, i.e. transmitting only the last cycles for “light” nodes (PR663 by Thomas Blanc, OCamlPro). Anyway, as Tezos will be used more and more, contexts will keep growing, and we need to keep decreasing the space and performance cost of Tezos storage.

As one part of our activity at OCamlPro is to allow companies to deploy their own private Tezos networks, we decided to experiment with new storage layouts. We implemented two branches: our branch IronTez1 is based on a full LMDB database, as Tezos currently, but with optimized storage representation ; our branch IronTez2 is based on a mixed database, with both LMDB and file storage.

To test these branches, we started a node from scratch, and recorded all the accesses to the context database, to be able to replay it with our new experimental nodes. The node took about 12 hours to synchronize with the network, on which about 3 hours were used to write and read in the context database. We then replayed the trace, either only the writes or with both reads and writes.

Here are the results:

The mixed storage is the most interesting: it uses half the storage of a standard Tezos node !

Again, the mixed storage is the most efficient : even with reads and writes, IronTez2 is five time faster than the current Tezos storage.

Finally, here is a graph that shows the impact of the two attacks that happened in November 2018, and how it can be mitigated by storage improvement:

The graph shows that, using mixed storage, it is possible to restore the storage growth of Tezos to what it was before the attack !

Interestingly, although these experiments have been done on full traces, our branches are completely backward-compatible : they could be used on an already existing database, to store the new contexts in our optimized format, while keeping the old data in the ancient format.

Of course, there is still a lot of work to do, before this work is finished. We think that there are still more optimizations that are possible, and we need to test our branches on running nodes for some time to get confidence (TzScan might be the first tester !), but this is a very encouraging work for the future of Tezos !