Merge remote-tracking branch 'upstream/master' into dev-michalis

13 files changed, 284 insertions, 123 deletions

diff --git a/.gitattributes b/.gitattributes
index 30dd12d..8c19733 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -1,4 +1,4 @@
 *.h linguist-language=C
 *.c linguist-language=C
 *.v linguist-language=Coq
-benchmarks/* linguist-vendored
+benchmarks/** linguist-vendored
diff --git a/CITATION.cff b/CITATION.cff
new file mode 100644
index 0000000..9328474
--- /dev/null
+++ b/CITATION.cff
@@ -0,0 +1,46 @@
+# -*- mode: yaml -*-
+cff-version: 1.2.0
+message: "If you use this software, please cite it as below."
+authors:
+- family-names: "Herklotz"
+  given-names: "Yann"
+  orcid: "https://orcid.org/0000-0002-2329-1029"
+- family-names: "Pollard"
+  given-names: "James D."
+  orcid: "https://orcid.org/0000-0003-1404-1527"
+- family-names: "Ramanathan"
+  given-names: "Nadesh"
+  orcid: "https://orcid.org/0000-0001-9083-8349"
+- family-names: "Wickerson"
+  given-names: "John"
+  orcid: "https://orcid.org/0000-0001-6735-5533"
+title: "Vericert"
+version: 1.2.1
+doi: 10.5281/zenodo.5093839
+date-released: 2021-07-12
+url: "https://github.com/ymherklotz/vericert"
+preferred-citation:
+  type: article
+  authors:
+  - family-names: "Herklotz"
+    given-names: "Yann"
+    orcid: "https://orcid.org/0000-0002-2329-1029"
+  - family-names: "Pollard"
+    given-names: "James D."
+    orcid: "https://orcid.org/0000-0003-1404-1527"
+  - family-names: "Ramanathan"
+    given-names: "Nadesh"
+    orcid: "https://orcid.org/0000-0001-9083-8349"
+  - family-names: "Wickerson"
+    given-names: "John"
+    orcid: "https://orcid.org/0000-0001-6735-5533"
+  doi: "10.1145/3485494"
+  journal: "Proc. ACM Program. Lang."
+  month: 11
+  pages: 30
+  title: "Formal Verification of High-Level Synthesis"
+  volume: 5
+  year: 2021
+  number: OOPSLA
+  publisher: Association for Computing Machinery
+  address: New York, NY, USA
diff --git a/LICENSE b/LICENSE
index edd3e1e..b386211 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,13 +1,3 @@
-Everything under src/ is licensed under the GPLv3 shown below, except for the
-following files:
-
-src/SoftwarePipeline/*: MIT
-
-    Copyright (c) 2008-2010 Jean-Baptiste Tristan and INRIA
-    Copyright (c) 2020-2021 Yann Herklotz
-
---------------------------------------------------------------------------------
-
                     GNU GENERAL PUBLIC LICENSE
                        Version 3, 29 June 2007
 
@@ -682,25 +672,3 @@ may consider it more useful to permit linking proprietary applications with
 the library.  If this is what you want to do, use the GNU Lesser General
 Public License instead of this License.  But first, please read
 <https://www.gnu.org/licenses/why-not-lgpl.html>.
-
---------------------------------------------------------------------------------
-
-Copyright (c) 2008,2009,2010 Jean-Baptiste Tristan and INRIA
-
-Permission is hereby granted, free of charge, to any person obtaining a copy
-of this software and associated documentation files (the "Software"), to deal
-in the Software without restriction, including without limitation the rights
-to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in
-all copies or substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-SOFTWARE.
diff --git a/Makefile b/Makefile
index 763c892..d14ef13 100644
--- a/Makefile
+++ b/Makefile
@@ -31,8 +31,10 @@ all: lib/COMPCERTSTAMP
 	$(MAKE) proof
 	$(MAKE) compile
 
-lib/COMPCERTSTAMP:
+lib/CompCert/Makefile.config: lib/CompCert/configure
 	(cd lib/CompCert && ./configure --ignore-coq-version $(ARCH))
+
+lib/COMPCERTSTAMP: lib/CompCert/Makefile.config
 	$(MAKE) HAS_RUNTIME_LIB=false CLIGHTGEN=false INSTALL_COQDEV=false -C lib/CompCert
 	touch $@
 
diff --git a/README.org b/README.org
index c2382f1..4426561 100644
--- a/README.org
+++ b/README.org
@@ -2,19 +2,17 @@
 
 #+html: <p align=center><a href="https://github.com/ymherklotz/vericert/actions"><img src="https://github.com/ymherklotz/vericert/workflows/CI/badge.svg" /></a>&nbsp;<a href="https://vericert.ymhg.org/"><img src="https://github.com/ymherklotz/vericert-docs/workflows/docs/badge.svg" /></a></p>
 
-A formally verified high-level synthesis (HLS) tool written in Coq,
-building on top of [[https://github.com/AbsInt/CompCert][CompCert]].
-This ensures the correctness of the C to Verilog translation according
-to our Verilog semantics and CompCert's C semantics, removing the need
-to check the resulting hardware for behavioural correctness.
+A formally verified high-level synthesis (HLS) tool written in Coq, building on top of [[https://github.com/AbsInt/CompCert][CompCert]].
+This ensures the correctness of the C to Verilog translation according to our Verilog semantics and
+CompCert's C semantics, removing the need to check the resulting hardware for behavioural
+correctness.
 
 ** Features
    :PROPERTIES:
    :CUSTOM_ID: features
    :END:
-The project is currently a work in progress, so proofs remain to be
-finished. Currently, the following C features are supported, but are not
-all proven correct yet:
+The project is currently a work in progress, so proofs remain to be finished. Currently, the
+following C features are supported, but are not all proven correct yet:
 
 - all int operations,
 - non-recursive function calls,
@@ -25,48 +23,38 @@ all proven correct yet:
    :PROPERTIES:
    :CUSTOM_ID: building
    :END:
-To build Vericert, the provided [[/Makefile][Makefile]] can be used.
-External dependencies are needed to build the project, which can be
-pulled in automatically with [[https://nixos.org/nix/][nix]] using the
-provided [[/default.nix][default.nix]] and [[/shell.nix][shell.nix]]
+To build Vericert, the provided [[/Makefile][Makefile]] can be used.  External dependencies are needed to build the
+project, which can be pulled in automatically with [[https://nixos.org/nix/][nix]] using the provided [[/default.nix][default.nix]] and [[/shell.nix][shell.nix]]
 files.
 
-The project is written in Coq, a theorem prover, which is extracted to
-OCaml so that it can then be compiled and executed. The dependencies of
-this project are the following:
-
-- [[https://coq.inria.fr/][Coq]]: theorem prover that is used to also
-  program the HLS tool.
-- [[https://ocaml.org/][OCaml]]: the OCaml compiler to compile the
-  extracted files.
-- [[https://github.com/mit-plv/bbv][bbv]]: an efficient bit vector
-  library.
-- [[https://github.com/ocaml/dune][dune]]: build tool for ocaml projects
-  to gather all the ocaml files and compile them in the right order.
-- [[http://gallium.inria.fr/~fpottier/menhir/][menhir]]: parser
-  generator for ocaml.
-- [[https://github.com/ocaml/ocamlfind][findlib]] to find installed
-  OCaml libraries.
+The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be
+compiled and executed. The dependencies of this project are the following:
+
+- [[https://coq.inria.fr/][Coq]]: theorem prover that is used to also program the HLS tool.
+- [[https://ocaml.org/][OCaml]]: the OCaml compiler to compile the extracted files.
+- [[https://github.com/mit-plv/bbv][bbv]]: an efficient bit vector library.
+- [[https://github.com/ocaml/dune][dune]]: build tool for ocaml projects to gather all the ocaml files and compile them in the right
+  order.
+- [[http://gallium.inria.fr/~fpottier/menhir/][menhir]]: parser generator for ocaml.
+- [[https://github.com/ocaml/ocamlfind][findlib]] to find installed OCaml libraries.
 - [[https://gcc.gnu.org/][GCC]]: compiler to help build CompCert.
 
-These dependencies can be installed manually, or automatically through
-Nix.
+These dependencies can be installed manually, or automatically through Nix.
 
 *** Downloading CompCert
     :PROPERTIES:
     :CUSTOM_ID: downloading-compcert
     :END:
-CompCert is added as a submodule in the =lib/CompCert= directory. It is
-needed to run the build process below, as it is the one dependency that
-is not downloaded by nix, and has to be downloaded together with the
-repository. To clone CompCert together with this project, you can run:
+CompCert is added as a submodule in the =lib/CompCert= directory. It is needed to run the build
+process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded
+together with the repository. To clone CompCert together with this project, you can run:
 
 #+begin_src shell
   git clone --recursive https://github.com/ymherklotz/vericert
 #+end_src
 
-If the repository is already cloned, you can run the following command
-to make sure that CompCert is also downloaded:
+If the repository is already cloned, you can run the following command to make sure that CompCert is
+also downloaded:
 
 #+begin_src shell
   git submodule update --init
@@ -76,12 +64,10 @@ to make sure that CompCert is also downloaded:
     :PROPERTIES:
     :CUSTOM_ID: setting-up-nix
     :END:
-Nix is a package manager that can create an isolated environment so that
-the builds are reproducible. Once nix is installed, it can be used in
-the following way.
+Nix is a package manager that can create an isolated environment so that the builds are
+reproducible. Once nix is installed, it can be used in the following way.
 
-To open a shell which includes all the necessary dependencies, one can
-use:
+To open a shell which includes all the necessary dependencies, one can use:
 
 #+begin_src shell
   nix-shell
@@ -93,8 +79,8 @@ which will open a shell that has all the dependencies loaded.
     :PROPERTIES:
     :CUSTOM_ID: makefile-build
     :END:
-If the dependencies were installed manually, or if one is in the
-=nix-shell=, the project can be built by running:
+If the dependencies were installed manually, or if one is in the =nix-shell=, the project can be built
+by running:
 
 #+begin_src shell
   make -j8
@@ -106,19 +92,50 @@ and installed locally, or under the =PREFIX= location using:
   make install
 #+end_src
 
-Which will install the binary in =./bin/vericert= by default. However,
-this can be changed by changing the =PREFIX= environment variable, in
-which case the binary will be installed in =$PREFIX/bin/vericert=.
+Which will install the binary in =./bin/vericert= by default. However, this can be changed by changing
+the =PREFIX= environment variable, in which case the binary will be installed in =$PREFIX/bin/vericert=.
 
 ** Running
    :PROPERTIES:
    :CUSTOM_ID: running
    :END:
-To test out =vericert= you can try the following examples which are in
-the test folder using the following:
+To test out =vericert= you can try the following examples which are in the test folder using the
+following:
 
 #+begin_src shell
   ./bin/vericert test/loop.c -o loop.v
   ./bin/vericert test/conditional.c -o conditional.v
   ./bin/vericert test/add.c -o add.v
 #+end_src
+
+** Citation
+
+If you use Vericert in any way, please cite it using our [[https://yannherklotz.com/papers/fvhls_oopsla21.pdf][OOPSLA'21 paper]]:
+
+#+begin_src bibtex
+@inproceedings{herklotz21_fvhls,
+  author = {Herklotz, Yann and Pollard, James D. and Ramanathan, Nadesh and Wickerson, John},
+  title = {Formal Verification of High-Level Synthesis},
+  year = {2021},
+  number = {OOPSLA},
+  numpages = {30},
+  month = {11},
+  journal = {Proc. ACM Program. Lang.},
+  volume = {5},
+  publisher = {Association for Computing Machinery},
+  address = {New York, NY, USA},
+  doi = {10.1145/3485494}
+}
+#+end_src
+
+** License
+
+This project is licensed under [[https://www.gnu.org/licenses/gpl-3.0.en.html][GPLv3]].  The license can be seen in [[/LICENSE][/LICENSE]].
+
+The following external code and its license is present in this repository:
+
+- [[/src/SoftwarePipelining][/src/SoftwarePipelining]] :: MIT
+
+#+begin_src text
+Copyright (c) 2008,2009,2010 Jean-Baptiste Tristan and INRIA
+#+end_src
diff --git a/default.nix b/default.nix
index 78ed487..762d38b 100644
--- a/default.nix
+++ b/default.nix
@@ -1,35 +1,15 @@
-with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/269fc4ddb896c1c5994eb4bb8c750ec18cb3db82.tar.gz") {};
+with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/8dd8bd8be74879f9f7919b16a4cb5ab2a75f18e5.tar.gz") {};
 let
-  ncoq = coq_8_12;
-  ncoqPackages = coqPackages_8_12;
-  bbv = ncoqPackages.callPackage
-    ( { coq, stdenv, fetchFromGitHub }:
-      stdenv.mkDerivation {
-        name = "coq${coq.coq-version}-bbv";
-
-        src = fetchFromGitHub {
-          owner = "mit-plv";
-          repo = "bbv";
-          rev = "5099237c52d2910f79a1a3ca9ae4dfa80129bf86";
-          sha256 = "0qnha333h7dc8105prdxvmkgy6l8swvyf6kz9v5s5dk4dvr5nra8";
-        };
-
-        buildInputs = with coq.ocamlPackages; [ ocaml camlp5 ];
-        propagatedBuildInputs = [ coq ];
-        enableParallelBuilding = true;
-
-        installPhase = ''
-          make -f Makefile.coq.all install COQLIB='$(out)/lib/coq/${coq.coq-version}/'
-        '';
-      } ) { };
+  ncoq = coq_8_13;
+  ncoqPackages = coqPackages_8_13;
 in
 stdenv.mkDerivation {
   name = "vericert";
   src = ./.;
 
   buildInputs = [ ncoq ncoqPackages.coqhammer cvc4 eprover z3-tptp dune_2 gcc
-                  ocaml ocamlPackages.findlib ocamlPackages.menhir
-                  ocamlPackages.ocamlgraph
+                  ncoq.ocaml ncoq.ocamlPackages.findlib ncoq.ocamlPackages.menhir
+                  ncoq.ocamlPackages.ocamlgraph
                 ];
 
   enableParallelBuilding = true;
diff --git a/docs b/docs
-Subproject f85153b7335ebf99ab6bf6e696b5a08fef38b61
+Subproject 3b2ce146bc6e651df8ac9910d08da05d88c06fb
diff --git a/lib/CompCert b/lib/CompCert
-Subproject c49caca4b5f0239b43610fbfe012d6ba0211b36
+Subproject 1daf96cdca4d828c333cea5c9a314ef86134298
diff --git a/scripts/docker/artifact.org b/scripts/docker/artifact.org
index 663afbf..fa0a936 100644
--- a/scripts/docker/artifact.org
+++ b/scripts/docker/artifact.org
@@ -9,9 +9,25 @@ This artifact should support the claims made in the paper "Formal Verification o
 - The cycle counts of Vericert on the benchmarks can be checked and compared against LegUp 4.0.
 - If Vivado is downloaded separately, then the whole performance section can be checked, including all the graphs that appear in the paper.
 
+** Artifact availability
+
+The artifact is available on Github, specifically on the ~oopsla21~ branch:
+
+https://github.com/ymherklotz/vericert
+
+#+latex: \noindent
+This release is also archived on Zenodo permanently:
+
+http://doi.org/10.5281/zenodo.5093839
+
+#+latex: \noindent
+However, for the purposes of this artifact review, a Docker image has been set up:
+
+https://hub.docker.com/repository/docker/ymherklotz/vericert
+
 ** Claims that are not supported by the artifact
 
-Unfortunately, we could not include our version of LegUp 4.0 in the artifact due to license restrictions.  In addition to that, LegUp was recently bought by Microchip and renamed to SmartHLS[fn:1], which means that it also cannot be freely downloaded anymore either, and the original open source version of LegUp 4.0 is not available anymore due to server issues in Toronto[fn:2].  We have tried contacting the authors of LegUp in Toronto, but have not heard back yet on if our version of LegUp can be shared in the artifact.
+Unfortunately, we could not include our version of LegUp 4.0 in the artifact due to license restrictions.  In addition to that, LegUp was recently bought by Microchip and renamed to SmartHLS[fn:1], which means that the most recent versions of LegUp are closed source and cannot be downloaded anymore.  The original open source version of LegUp 4.0 is not currently available either at the moment. The LegUp team have advised us that this is due to server issues in Toronto.[fn:2] We have not heard back from them about whether it is ok for us to share our copy of LegUp 4.0 for artifact evaluation purposes, so we have not done so.
 
 Instead, we have included the net lists that LegUp generated from the benchmarks in the artifact, with all the optimisation levels that were tried, however, it does mean that these cannot be verified again and that other optimisation options cannot be tried.
 
@@ -29,18 +45,35 @@ docker run -it ymherklotz/vericert:1.0 sh
 Then, one just has to go into the directory which contains the git repository (~/vericert~) and open a ~nix-shell~, which will load a shell with all the correct dependencies loaded:
 
 #+begin_src shell
+cd /vericert
 nix-shell
 #+end_src
 
-Then, any commands can be run in this shell to run ~vericert~, which has already been compiled and can be found in the ~/vericert/bin~ directory.  For a quick test that it is working, a few very simple examples in the ~/vericert/test~ directory can be run by using the following inside of the ~/vericert~ directory:
+Then, all commands can be run in this shell, as well as ~vericert~, which has already been compiled and can be found in the ~/vericert/bin~ directory.  For a quick test that it is working, a few very simple examples in the ~/vericert/test~ directory can be run by using the following inside of the ~/vericert~ directory:
 
 #+begin_src shell
+cd /vericert
 make test
 #+end_src
 
 If this finishes without errors, it means that Vericert is working correctly.
 
-* Detailed Artifact Description
+Finally, to check that the benchmarks work correctly as well, we can quickly compile and run one as well:
+
+#+begin_src shell
+cd /vericert/benchmarks/polybench-syn
+make
+./stencils/jacobi-1d
+#+end_src
+
+This simulates the hardware design generated for the jacobi-1d benchmark in PolyBench/C, and should print the return value: 1, as well as the cycle count: 19996 as follows:
+
+#+begin_src shell
+cycles: 19996
+finished: 1
+#+end_src
+
+* Step-by-Step instructions
 
 This section describes the detailed instructions to get the results for the different sections of the paper, first describing the structure of the proof and how to execute Vericert manually, to finally running Vericert on the benchmarks and get the cycle counts for the Vericert designs as well as the precompiled LegUp designs.
 
@@ -60,7 +93,63 @@ The main directory structure of Vericert is the following:
 
 ** Description of the proof
 
-The proof is mostly located in ~/src/hls~, which contains the proof of correctness of the 3AC to HTL transformation, as well as the transformation from HTL to Verilog.  Any other files in the ~/src/hls~ directory that are not mentioned below are there for future optimisations such as scheduling, which are not used.
+The proof is mostly located in ~/src/hls~, which contains the proof of correctness of the 3AC to HTL transformation, as well as the transformation from HTL to Verilog.  First, we will describe where each section of the paper is implemented, then a description of all the files in the src directory will be included.
+
+*** Implementation of paper sections
+
+When mentioning Coq source files, they will always be relative to the ~/vericert/src~ directory in the docker image.
+
+**** Section 2
+
+- Figure 2 :: This example is not included in the repository or docker image, however, if the small C example in Figure 2a is copied into a file ~main.v~, it can be compiled using the following:
+
+#+begin_src shell
+vericert -o main.v -O0 -drtl -dhtl main.c
+#+end_src
+
+Where ~-O0~ means it will not apply any CompCert optimisations, ~-drtl~ means it will print the internal 3AC (also known as RTL) representation and ~-dhtl~ outputs the HTL representation.  After running that command, Figure 2b should be the exact same as the ~main.rtl.7~ file that was generated, and Figure 2c should be the same as ~main.v~, with some slight modifications to some variable names and formatting.
+
+- Figure 3 :: After running the above command, Figure 3 will be a visual representation of ~main.
+
+- Section 2.2.2 :: The abstract RAM description and is used in HTL can be found in ~hls/HTL.v:139~. This also corresponds to Figure 7. This abstract description is then implemented as a concrete Verilog implementation shown in ~hls/Veriloggen.v:45~.  The proof that the Verilog implementation is correct according to the HTL specification of it can be found in Lemma ~ram_exec_match~, ~hls/Veriloggenproof.v:284~.
+
+- Section 2.2.3 :: This proof is for Theorem ~shrx_shrx_alt_equiv~, ~common/Integer~\-~Extra.v:661~.
+
+**** Section 3
+
+This Section is mainly implemented in ~hls/Verilog.v~.
+
+- Module execution rule :: The updated negative edge execution rule can be found in ~hls/Verilog.v:582~ which is called ~step_module~, and has a ~mis_stepp~ and ~mis_stepp_negedge~ for the steps of the positive and negative edge triggered always blocks.
+
+- Figure 5 :: This is implemented as all the other possible steps in one Verilog step, shown in ~hls/Verilog.v:581~.  The Figure just uses some nicer notation for the inference rules.
+
+- Figure 6 :: Our dependenty typed arrays used for the memory model are implemented in ~hls/Array.v~, and is then integrated in the Verilog semantics properly using the ~arr_associations~ type, defined in ~hls/Verilog.v:60~, which is a blocking and nonblocking array where each element is an optional, as shown in Figure 6.
+
+**** Section 5
+
+- Theorem 1 :: This is proven as Theorem ~transf_c_program_correct~ in ~Compiler.v~\-~:415~.
+
+- Lemma 1 :: This is proven as part of Theorem ~cstrategy_semantic_preservation~ in ~Compiler.v:334~, which also proves the backward simulation at the same time.
+
+- Lemma 2 :: The specification of the translation from 3AC to HTL is shown in Theorem ~transl_module_correct~ in ~hls/HTLgenspec.v:608~ and is called ~tr_module~ instead of ~spec_htl~ as in the paper, and ~tr_htl~ is called ~transl_~\-~module~ instead.
+
+- Section 4.1.2, ~match_states~ :: The ~match_states~ property to match two states in 3AC and HTL up is defined in ~hls/HTLgenproof.v:112~.
+
+- Lemma 3 :: Proven as Theorem ~transl_step_correct~ in ~hls/HTLgenproof.v:2856~ and describes the simulation diagram shown in the paper.
+
+- Section 4.2.1 :: The specification of the store is located in ~hls/Memorygen.v:2096~ and is called ~alt_store~.
+
+- Section 4.2.2, ~match_states~ :: The definition of matching states is defined in ~hls~\-~/Memory~\-~gen.v:314~, where ~ARRS_SIZE~ corresponds to the property of equally sized arrays at each step and ~DISABLE_RAM~ corresponds to the property that the RAM is always disabled by default.
+
+- Lemma 4 :: There is a small typo in the paper, and this Lemma should describe the forward simulation of the insertion of the RAM.  This is proven in Theorem ~transf_program_correct~ in ~hls/Memorygen.v:3196~, and the simulation diagram for this translation is proven in Theorem ~transf_step_correct~ in ~hls/Memorygen.v:3000~.
+
+- Lemma 5 :: This is proven in Theorem ~transf_program_correct~ in ~hls/Veriloggen~\-~proof.v:537~.  The assumption that the HTL module and Verilog module are related by ~transl_program~ (~tr_verilog~ in the paper) is given in the hypothesis ~TRANSL~ in ~hls/Veriloggenproof.v:343~.
+
+- Lemma 6 :: The determinism of the Verilog semantics is proven in ~semantics_deter~\-~minate~ in ~hls/Verilog.v:810~.
+
+- Table 1 :: These values were calculated by hand to separate specification, implementation and proof code.  The raw results can be found in the last table in the ~/data/data/results.org~ file, or in the ~/data/data/code-count.csv~.
+
+*** Description of files
 
 - ~/src/Compiler.v~ :: The very top-level of the proof is located here and it contains the main proof of the compiler, which is the proof that the ~transf_hls~ function is correct, which takes C and outputs Verilog.  The main proof of correctness is in the Theorem called ~transf_c_program_correct~, which says that if the ~transf_hls~ function succeeded, that the backward simulation should hold between C and Verilog.
 - ~/src/common~ :: This directory contains some common library extensions and proofs that are used in other parts of Vericert.  This includes the proof of correctness of Section 2.2.3, which is located in ~/src/common/IntegerExtra.v~ under the Theorem ~shrx_shrx_alt_equiv~.
@@ -214,9 +303,28 @@ Then, using the hash it can be run in the same way as the docker container that
 docker run -it <hash> sh
 #+end_src
 
+** Building from git without Docker.
+
+The only dependency that is require is nix[fn:7].  Once that is installed, we can clone the Github repository and checkout the ~oopsla21~ branch:
+
+#+begin_src shell
+git clone https://github.com/ymherklotz/vericert
+cd vericert
+git checkout oopsla21
+#+end_src
+
+Then, it can be compiled and installed using:
+
+#+begin_src shell
+nix-shell --run "make -j7"
+nix-shell --run "make install"
+nix-shell --run "./bin/vericert ./test/add.c -o add.v"
+#+end_src
+
 * Footnotes
 
 
+[fn:7] https://nixos.org/download.html
 [fn:6] https://imperialcollegelondon.box.com/s/nqoaquk7j5mj70db16s6bdbhg44zjn52
 [fn:5] https://imperialcollegelondon.box.com/s/94clcbjowla3987opf3icjz087ozoi1o
 [fn:4] https://imperialcollegelondon.box.com/s/ril1utuk2n88fhoq3375oxiqcgw42b8a
diff --git a/scripts/docker/artifact.pdf b/scripts/docker/artifact.pdf
index 28e6f7a..05ec4fd 100644
--- a/scripts/docker/artifact.pdf
+++ b/scripts/docker/artifact.pdf
diff --git a/src/SoftwarePipelining/LICENSE b/src/SoftwarePipelining/LICENSE
new file mode 100644
index 0000000..e275fa0
--- /dev/null
+++ b/src/SoftwarePipelining/LICENSE
@@ -0,0 +1,19 @@
+Copyright (c) 2008,2009,2010 Jean-Baptiste Tristan and INRIA
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml
index a2700a1..a5fa554 100644
--- a/src/hls/PrintVerilog.ml
+++ b/src/hls/PrintVerilog.ml
@@ -75,7 +75,7 @@ let pprint_binop l r =
 
 let unop = function
   | Vneg -> " - "
-  | Vnot -> " ! "
+  | Vnot -> " ~ "
 
 let register a =
   match PMap.find_opt a !name_map with
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 5e123a3..3fab464 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -183,23 +183,44 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) :
      | Pvar p' => Some (exist _ (((true, p') :: nil) :: nil) _)
      | Pand p1 p2 =>
       match trans_pred n p1, trans_pred n p2 with
-      | Some (exist p1' _), Some (exist p2' _) =>
+      | Some (exist _ p1' _), Some (exist _ p2' _) =>
         Some (exist _ (p1' ++ p2') _)
       | _, _ => None
       end
      | Por p1 p2 =>
       match trans_pred n p1, trans_pred n p2 with
-      | Some (exist p1' _), Some (exist p2' _) =>
+      | Some (exist _ p1' _), Some (exist _ p2' _) =>
         Some (exist _ (mult p1' p2') _)
       | _, _ => None
       end
      | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _)
-     | _ => None
+     | Pnot (Pnot p') =>
+       match trans_pred n p' with
+       | Some (exist _ p1' _) => Some (exist _ p1' _)
+       | None => None
+       end
+     | Pnot (Pand p1 p2) =>
+       match trans_pred n (Por (Pnot p1) (Pnot p2)) with
+       | Some (exist _ p1' _) => Some (exist _ p1' _)
+       | None => None
+       end
+     | Pnot (Por p1 p2) =>
+       match trans_pred n (Pand (Pnot p1) (Pnot p2)) with
+       | Some (exist _ p1' _) => Some (exist _ p1' _)
+       | None => None
+       end
      end
    end); split; intros; simpl in *; auto.
   - inv H. inv H0; auto.
-  - admit.
-  - admit.
+  - split; auto. destruct (a p') eqn:?; crush.
+  - inv H. inv H0. unfold satLit in H. simplify. rewrite H. auto.
+    crush.
+  - rewrite negb_involutive in H. apply i in H. auto.
+  - rewrite negb_involutive. apply i; auto.
+  - rewrite negb_andb in H. apply i. auto.
+  - rewrite negb_andb. apply i. auto.
+  - rewrite negb_orb in H. apply i. auto.
+  - rewrite negb_orb. apply i. auto.
   - apply satFormula_concat.
     apply andb_prop in H. inv H. apply i in H0. auto.
     apply andb_prop in H. inv H. apply i0 in H1. auto.
@@ -211,16 +232,16 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) :
   - apply orb_true_intro.
     apply satFormula_mult2 in H. inv H. apply i in H0. auto.
     apply i0 in H0. auto.
-Abort.
+Qed.
 
-(*Definition sat_pred (bound: nat) (p: pred_op) :
+Definition sat_pred (bound: nat) (p: pred_op) :
   option ({al : alist | sat_predicate p (interp_alist al) = true}
           + {forall a : asgn, sat_predicate p a = false}).
   refine
   ( match trans_pred bound p with
-    | Some (exist fm _) =>
+    | Some (exist _ fm _) =>
       match boundedSat bound fm with
-      | Some (inleft (exist a _)) => Some (inleft (exist _ a _))
+      | Some (inleft (exist _ a _)) => Some (inleft (exist _ a _))
       | Some (inright _) => Some (inright _)
       | None => None
       end
@@ -234,7 +255,7 @@ Qed.
 
 Definition sat_pred_simple (bound: nat) (p: pred_op) :=
   match sat_pred bound p with
-  | Some (inleft (exist al _)) => Some (Some al)
+  | Some (inleft (exist _ al _)) => Some (Some al)
   | Some (inright _) => Some None
   | None => None
   end.
@@ -243,7 +264,7 @@ Definition sat_pred_temp (bound: nat) (p: pred_op) :=
   match trans_pred_temp bound p with
   | Some fm => boundedSatSimple bound fm
   | None => None
-  end.*)
+  end.
 
 Inductive instr : Type :=
 | RBnop : instr