Overview

This repository contains a backend for the saw-core library that outputs terms in the syntax of Coq. The Coq files generated by this backend depend on the Coq support libraries described below, which must be compiled in Coq in order to be used.

The Coq Support Libraries

The Coq files that are generated by the saw-core-coq backend rely on a number of support libraries, some of which are generated from the SAW core prelude files and some of which are hand-written extensions of those libraries. These support libraries must be compiled by Coq in order to use them.

Installing Dependencies

To compile the Coq support libraries, Coq must be installed, as must the following Coq library:

• bits

The recommended way to install Coq and these dependencies is using opam. This can be done with the following steps, which will not only install opam, Coq, and the above mentioned Coq libraries, but will make sure to install the proper version of Coq needed for those libraries:

sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)
opam init
opam repo add coq-released https://coq.inria.fr/opam/released
opam install -y coq-bits
opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#62e916fe308d7b215363b80edf9e6d6d1602c737

We have pinned the entree-specs dependency's commit to ensure that it points to a known working version. If you are an advanced user who wishes to use the latest `entree-specs commit, you can ommit the commit hash:

opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git

If you run into any issue that is probably due to the version mismatch between the ocamlc and the ocaml base system installed on your machine and it can be fixed as explained here.

Currently, the Coq support libraries for saw-core-coq requires Coq 8.15. Note that the entree-specs dependency does not currently build with Coq 8.16 (see this issue).

Building the and Using the Coq Support Libraries

The coq/ directory contains the Coq support libraries for the saw-core-coq backend, as well as a number of example Coq files that have been generated from existing SAW proofs. In order to build just the Coq support libraries, the following commands can be used:

cd coq
make generated/CryptolToCoq/SAWCorePrelude.vo

To use these libraries, the following lines can be added to a _CoqProject file, where PATH_TO_SAW is replaced by the path to the saw-script directory:

-Q PATH_TO_SAW/saw-core-coq/coq/generated/CryptolToCoq   CryptolToCoq
-Q PATH_TO_SAW/saw-core-coq/coq/handwritten/CryptolToCoq   CryptolToCoq

Generating the Coq Support Libraries

The Coq support libraries can be re-generated from their SAWCore/Cryptol counterparts if these modules change. This can be done in the saw/ directory, by running the scripts there with an appropriate version of the saw executable. The output of such files are currently being version-controlled, as a way of keeping track of their evolution.

/path/to/saw generate_scaffolding.saw

Directory Structure

• coq/ contains handwritten Coq files in handwritten/ and generated ones in generated/, as well as some files needed to build the Coq files.

• cryptol/ contains some Cryptol files that we care about extracting.

• saw/ contains SAW scripts that generate the Coq files.

Coq Files Organization

The Coq files have a somewhat complex organization. We demonstrate the current dependencies, ignoring transitive dependencies for clarity:

                      SAWCoreScaffolding (H)
                          /           \
SAWCoreVectorsAsCoqVectors (H)   SAWCoreVectorsAsCoqLists (H)
                          \           /
  CoqVectorsExtra (H)    SAWCorePrelude (G)
             \            /            \
   CryptolPrimitivesForSAWCore (G)     SAWCorePreludeExtra (H)
                         \               /
               CryptolPrimitivesForSAWCoreExtra (H)

(G) stands for generated files, while (H) stands for handwritten files.

• SAWCoreScaffolding defines some of SAW core primitive types and values.

• SAWCoreVectorsAsCoqVectors and SAWCoreVectorsAsCoqLists are two realizations of the vector type, the latter ignoring the type index. In practice, we have found that the latter is a no-go for proofs unless values are packaged with a proof that their length is equal to the index.

• SAWCorePrelude is generated from Prelude.sawcore, available in the saw-core project.

• CoqVectorsExtra contains facts about vectors that the Coq standard library does not provide.

• CryptolPrimitivesForSAWCore is generated from Cryptol.sawcore, available in the cryptol-saw-core project.

• SAWCorePreludeExtra defines useful functions for CryptolPrimitivesForSAWCoreExtra to use.

• CryptolPrimitivesForSAWCoreExtra contains some additional useful definitions.

Acknowledgements

This material is based upon work supported by the Office of Naval Research under Contract No. N68335-17-C-0452. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Office of Naval Research.