README

# Store buffer proofs in Coq
This repository contains proofs related to store buffers in Coq.

## Files
In `src/` stand multiple files:

 - `definitions.v`: defines multiple common types, functions and lemmas. Some
   may be useless.
 - `utils.v`: defines missing theorems and lemmas in the stdlib. Some may also
   be useless.
 - `storebuffer.v`: defines a parallel store buffer with granular locking, and
   proves that it is monotonic. The proofs has multiple problems (it does not
   take store buffer state changes into account, for instance), so this file
   should be disregarded altogether. Also, lots of useless theorems. See this as
   a playing ground for the next proofs.
 - `correct_storebuffer.v`: defines a parallel store buffer with full locking,
   and proves that it is monotonic.
 - `granular_sb.v`: another parallel store buffer with granular locking, but
   this time prove that it does not work when taking the state of the store
   buffer into account.  This is done by finding a counter-example.

## Dependencies
This project was written with Coq 8.15.2, but it should work with Coq 8.14+. It
will not work with older versions of Coq, because it uses some theorems that
appeared in Coq 8.14.

No external dependencies are used, and proofs are made in Ltac.

## Building
Assuming that you have Coq 8.14+ in your path. Execute the following commands in
the root of the project:

``` sh
$ coq_makefile -f _CoqProject -o Makefile
$ make
```