Dexter version: 4e24123.

The formal specification is based on the informal specification dated
September 31, 2020.

This is a joint work by:
 - Arvid Jakobsson, Nomadic Labs
 - Kristina Sojakova, INRIA
 - Colin González, Nomadic Labs