This code was primarily written by Karthikeyan Bhargavan (INRIA) and Benjamin Beurdouche (INRIA)