coq-vsu-int63 Documentation

Introduction

A Verified Software Unit for 63-bit integer arithmetic.

Implemented in C, modeled in Coq, and proven correct using the Verified Software Toolchain.

Compatible with CompCert.

Using the C library

To use the library, simply include the header file:

#include <coq-vsu-int63/int63.h>

Alternatively, you can include the entire implementation:

#include <coq-vsu-int63/src/int63.c>

The library is installed to the location given by vsu -I. You can bring this location into your compiler's search path by passing -I`vsu -I` to your compiler at build time.

An API reference is provided in int63.h.