Fix documentation generation

4 files changed, 625 insertions, 330 deletions

diff --git a/doc/Makefile.extr b/doc/Makefile.extr
index 9d4f361..ef72270 100644
--- a/doc/Makefile.extr
+++ b/doc/Makefile.extr
@@ -9,13 +9,20 @@ install-deps:
 %.html: %.org
 	emacs --batch --file $< --load ./res/publish.el --funcall org-html-export-to-html
 
-manual:
-	mkdir -p manual
+vericert.texi: documentation.org ./res/publish.el
 	emacs --batch --file documentation.org --load ./res/publish.el --funcall org-texinfo-export-to-texinfo
+
+manual: vericert.texi
+	mkdir -p manual
 	makeinfo --html --number-sections --no-split \
         --css-ref "https://www.gnu.org/software/emacs/manual.css" \
         vericert.texi -o ./manual/index.html
-	cp -r images ./manual/.
+# cp -r images ./manual/.
+
+manual-split: vericert.texi
+	makeinfo --html --number-sections --split=section \
+        --css-ref "https://www.gnu.org/software/emacs/manual.css" \
+        vericert.texi -o ./manual-split
 
 man-html: man.html
 	mkdir -p man
diff --git a/doc/documentation.org b/doc/documentation.org
index 5a1bf61..d5ed16d 100644
--- a/doc/documentation.org
+++ b/doc/documentation.org
@@ -1,7 +1,7 @@
 #+title: Vericert Manual
 #+subtitle: Release {{{version}}}
 #+author:   Yann Herklotz
-#+email:    git@ymhg.org
+#+email:    git@yannherklotz.com
 #+language: en
 
 * Introduction
@@ -132,9 +132,105 @@ $ echo $?
 50
 #+end_src
 
-** Man pages
+** Running Vericert on the PolyBench/C benchmarks
 
-#+transclude: [[file:man.org][file:man.org]] :exclude-elements "keyword" :level 3
+The main benchmark that is currently used to run Vericert is [[http://web.cse.ohio-state.edu/~pouchet.2/software/polybench/][PolyBench/C]], which
+was slightly modified to make it run through Vericert.  There are two versions
+of this benchmark available: PolyBench/C with and without divisions.  In the
+version of the benchmark without division, the division C operator =/= and
+modulus operator was replaced by a function performing a numerical division
+and modulus called: =divide=, =sdivide=, =modulo= and =smodulo=.
+
+Vericert also does not support =printf=, which are used to produce the golden
+output using GCC.  They are therefore placed within an =ifndef SYNTHESIS= block.
+To successfully run vericert on these benchmarks one therefore needs to use the
+=-DSYNTHESIS= flag.
+
+*** Example running a single benchmark
+
+To run a single benchmark, navigate to the benchmark directory, which from the
+root of the repository (which I will be referencing using =$VERICERT_ROOT=)
+would be:
+
+#+begin_src shell
+VERICERT_ROOT=$(git rev-parse --show-toplevel)
+cd $VERICERT_ROOT/benchmarks/polybench-syn
+#+end_src
+
+Then, to run the =jacobi-1d= benchmark, one can go into the directory that
+contains the benchmark, which in this case is =stencils=:
+
+#+begin_src shell
+cd stencils
+#+end_src
+
+And one can then translate =jacobi-1d.c= to hardware using Vericert by using the
+following (assuming that vericert was built using =make && make install=, which
+places the =vericert= in =$VERICERT_ROOT/bin=):
+
+#+begin_src shell
+make VERICERT=$VERICERT_ROOT/bin/vericert VERICERT_OPTS="-DSYNTHESIS" jacobi-1d.sv
+#+end_src
+
+**** Running Simulations
+
+Setting the =VERICERT= and =VERICERT_OPTS= variables can also be done by
+modifying the first two lines of the
+=$VERICERT_ROOT/benchmarks/polybench-syn/common.mk= file, which might be more
+convenient than having to set the settings on every =Makefile= run.  In the next
+sections I will assume that these settings have been set in the =common.mk=
+file, and so will not specify them on the commandline anymore.
+
+Simulations for the SystemVerilog design can be generated using the following:
+
+#+begin_src shell
+# Building Icarus Verilog simulation
+make jacobi-1d.iver
+# Running Icarus Verilog simulation
+./jacobi-1d.iver
+# Building Verilator simulation
+make jacobi-1d.verilator
+# Running Verilator simulation
+./jacobi-1d.verilator/Vmain
+#+end_src
+
+**** Producing the golden GCC result
+
+To produce the golden GCC result to check for the correctness of the simulation
+result, the following command can be used:
+
+#+begin_src shell
+# Compile C code using gcc
+make jacobi-1d.gcc
+# Run the GCC code
+./jacobi-1d.gcc
+#+end_src
+
+It should produce the same =finish= result as the SystemVerilog simulation.
+
+*** Running all benchmarks
+
+To run vericert on all benchmarks and simulate them all, one can use the base
+=Makefile= in addition to the =$VERICERT_ROOT/scripts/run-vericert.sh= script.
+
+#+begin_src shell
+# Build all the benchmarks using vericert, iverilog, verilator and GCC
+cd $VERICERT_ROOT/benchmarks/polybench-syn
+make
+# Run all the simulations and compare against the GCC golden output
+$VERICERT_ROOT/scripts/run-vericert.sh
+#+end_src
+
+This should produce a file containing the cycle counts for each benchmark, which
+can be viewed using:
+
+#+begin_src shell
+cat $VERICERT_ROOT/scripts/exec.csv
+#+end_src
+
+* Man Page
+
+#+transclude: [[file:man.org][file:man.org]] :exclude-elements "keyword" :level 2
 
 * Unreleased Features
 :PROPERTIES:
diff --git a/doc/res/install-deps.el b/doc/res/install-deps.el
index 09cf4ae..6720437 100644
--- a/doc/res/install-deps.el
+++ b/doc/res/install-deps.el
@@ -8,4 +8,5 @@
 (package-install 'org)
 (package-install 'org-contrib)
 (package-install 'org-transclusion)
+(package-install 'ox-rst)
 (package-install 'htmlize)
diff --git a/doc/vericert.rst b/doc/vericert.rst
index 19ac28f..8547179 100644
--- a/doc/vericert.rst
+++ b/doc/vericert.rst
@@ -1,306 +1,484 @@
-===============
-Vericert Manual
-===============
-
+.. _docs:
 
 Introduction
-------------
+============
+
+Vericert translates C code into a hardware description language called
+Verilog, which can then be synthesised into hardware, to be placed onto
+a field-programmable gate array (FPGA) or application-specific
+integrated circuit (ASIC).
+
+.. figure:: ./images/toolflow.png
+   :alt: 
+
+The design shown in Figure `fig:design <fig:design>`__ shows how
+Vericert leverages an existing verified C compiler called
+`CompCert <https://compcert.org/compcert-C.html>`__ to perform this
+translation.
 
-Vericert translates C code into a hardware description language called Verilog, which can then be
-synthesised into hardware, to be placed onto a field-programmable gate array (FPGA) or
-application-specific integrated circuit (ASIC).
+.. raw:: texinfo
 
-.. _fig:design:
+   @insertcopying
 
-.. figure:: /_static/images/toolflow.svg
+COPYING
+=======
 
-    Current design of Vericert, where HTL is an intermediate language representing a finite state
-    machine with data-path (FSMD) and Verilog is the target language.
+Copyright (C) 2019-2022 Yann Herklotz.
 
-The design shown in Figure `fig:design`_ shows how Vericert leverages an existing verified C
-compiler called `CompCert <https://compcert.org/compcert-C.html>`_ to perform this translation.
+   Permission is granted to copy, distribute and/or modify this document
+   under the terms of the GNU Free Documentation License, Version 1.3 or
+   any later version published by the Free Software Foundation; with no
+   Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. A
+   copy of the license is included in the section entitled \``GNU Free
+   Documentation License''.
 
 .. _building:
 
 Building Vericert
------------------
+=================
+
+.. raw:: org
+
+   #+transclude: [[file:~/projects/vericert/README.org::#building][file:../README.org::#building]] :only-contents :exclude-elements "headline property-drawer"
+
+.. raw:: org
+
+   #+transclude: [[file:~/projects/vericert/README.org::#downloading-compcert][file:../README.org::#downloading-compcert]] :level 2
 
+.. raw:: org
+
+   #+transclude: [[file:~/projects/vericert/README.org::#setting-up-nix][file:../README.org::#setting-up-nix]] :level 2
+
+.. raw:: org
+
+   #+transclude: [[file:~/projects/vericert/README.org::#makefile-build][file:../README.org::#makefile-build]] :level 2
 
 Testing
-~~~~~~~
+-------
 
-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:
 
 .. code:: 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
+   ./bin/vericert test/loop.c -o loop.v
+   ./bin/vericert test/conditional.c -o conditional.v
+   ./bin/vericert test/add.c -o add.v
 
 Or by running the test suite using the following command:
 
 .. code:: shell
 
-    make test
-
-.. _using-vericert:
+   make test
 
 Using Vericert
---------------
+==============
+
+Vericert can be used to translate a subset of C into Verilog. As a
+simple example, consider the following C file (``main.c``):
+
+.. code:: c
+
+   void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) {
+       int sum = 0;
+       for (int c = 0; c < 2; c++) {
+           for (int d = 0; d < 2; d++) {
+               for (int k = 0; k < 2; k++) {
+                   sum = sum + first[c][k]*second[k][d];
+               }
+               multiply[c][d] = sum;
+               sum = 0;
+           }
+       }
+   }
+
+   int main() {
+       int f[2][2] = {{1, 2}, {3, 4}};
+       int s[2][2] = {{5, 6}, {7, 8}};
+       int m[2][2] = {{0, 0}, {0, 0}};
+
+       matrix_multiply(f, s, m);
+       return m[1][1];
+   }
+
+It can be compiled using the following command, assuming that vericert
+is somewhere on the path.
 
-Vericert can be used to translate a subset of C into Verilog.  As a simple example, consider the
-following C file (``main.c``):
+.. code:: shell
 
-.. code:: C
+   vericert main.c -o main.v
 
-    void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) {
-        int sum = 0;
-        for (int c = 0; c < 2; c++) {
-            for (int d = 0; d < 2; d++) {
-                for (int k = 0; k < 2; k++) {
-                    sum = sum + first[c][k]*second[k][d];
-                }
-                multiply[c][d] = sum;
-                sum = 0;
-            }
-        }
-    }
+The Verilog file contains a top-level test-bench, which can be given to
+any Verilog simulator to simulate the hardware, which should give the
+same result as executing the C code. Using `Icarus
+Verilog <http://iverilog.icarus.com/>`__ as an example:
 
-    int main() {
-        int f[2][2] = {{1, 2}, {3, 4}};
-        int s[2][2] = {{5, 6}, {7, 8}};
-        int m[2][2] = {{0, 0}, {0, 0}};
+.. code:: shell
 
-        matrix_multiply(f, s, m);
-        return m[1][1];
-    }
+   iverilog -o main_v main.v
 
-It can be compiled using the following command, assuming that vericert is somewhere on the path.
+When executing, it should therefore print the following:
 
 .. code:: shell
 
-    vericert main.c -o main.v
+   $ ./main_v
+   finished: 50
 
-The Verilog file contains a top-level test-bench, which can be given to any Verilog simulator to
-simulate the hardware, which should give the same result as executing the C code.  Using `Icarus
-Verilog <http://iverilog.icarus.com/>`_ as an example:
+This gives the same result as executing the C in the following way:
 
 .. code:: shell
 
-    iverilog -o main_v main.v
+   $ gcc -o main_c main.c
+   $ ./main_c
+   $ echo $?
+   50
 
-When executing, it should therefore print the following:
+Running Vericert on the PolyBench/C benchmarks
+----------------------------------------------
+
+The main benchmark that is currently used to run Vericert is
+`PolyBench/C <http://web.cse.ohio-state.edu/~pouchet.2/software/polybench/>`__,
+which was slightly modified to make it run through Vericert. There are
+two versions of this benchmark available: PolyBench/C with and without
+divisions. In the version of the benchmark without division, the
+division C operator ``/`` and modulus operator was replaced by a
+function performing a numerical division and modulus called: ``divide``,
+``sdivide``, ``modulo`` and ``smodulo``.
+
+Vericert also does not support ``printf``, which are used to produce the
+golden output using GCC. They are therefore placed within an
+``ifndef SYNTHESIS`` block. To successfully run vericert on these
+benchmarks one therefore needs to use the ``-DSYNTHESIS`` flag.
+
+Example running a single benchmark
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+To run a single benchmark, navigate to the benchmark directory, which
+from the root of the repository (which I will be referencing using
+``$VERICERT_ROOT``) would be:
 
 .. code:: shell
 
-    $ ./main_v
-    finished: 50
+   VERICERT_ROOT=$(git rev-parse --show-toplevel)
+   cd $VERICERT_ROOT/benchmarks/polybench-syn
 
-This gives the same result as executing the C in the following way:
+Then, to run the ``jacobi-1d`` benchmark, one can go into the directory
+that contains the benchmark, which in this case is ``stencils``:
 
 .. code:: shell
 
-    $ gcc -o main_c main.c
-    $ ./main_c
-    $ echo $?
-    50
+   cd stencils
 
-Man pages
-~~~~~~~~~
+And one can then translate ``jacobi-1d.c`` to hardware using Vericert by
+using the following (assuming that vericert was built using
+``make && make install``, which places the ``vericert`` in
+``$VERICERT_ROOT/bin``):
 
-.. _unreleased-features:
+.. code:: shell
 
-Unreleased Features
--------------------
+   make VERICERT=$VERICERT_ROOT/bin/vericert VERICERT_OPTS="-DSYNTHESIS" jacobi-1d.sv
 
-The following are unreleased features in Vericert that are currently being worked on and have not
-been completely proven correct yet.  Currently this includes features such as:
+#. Running Simulations
 
-- `scheduling`_,
+   Setting the ``VERICERT`` and ``VERICERT_OPTS`` variables can also be
+   done by modifying the first two lines of the
+   ``$VERICERT_ROOT/benchmarks/polybench-syn/common.mk`` file, which
+   might be more convenient than having to set the settings on every
+   ``Makefile`` run. In the next sections I will assume that these
+   settings have been set in the ``common.mk`` file, and so will not
+   specify them on the commandline anymore.
 
-- `operation-chaining`_,
+   Simulations for the SystemVerilog design can be generated using the
+   following:
 
-- `if-conversion`_, and
+   .. code:: shell
 
-- `functions`_.
+      # Building Icarus Verilog simulation
+      make jacobi-1d.iver
+      # Running Icarus Verilog simulation
+      ./jacobi-1d.iver
+      # Building Verilator simulation
+      make jacobi-1d.verilator
+      # Running Verilator simulation
+      ./jacobi-1d.verilator/Vmain
 
-This page gives some preliminary information on how the features are implemented and how the proofs
-for the features are being done.  Once these features are properly implemented, they will be added
-to the proper documentation.
+#. Producing the golden GCC result
 
-.. _scheduling:
+   To produce the golden GCC result to check for the correctness of the
+   simulation result, the following command can be used:
 
-Scheduling
-~~~~~~~~~~
+   .. code:: shell
 
-Scheduling is an optimisation which is used to run various instructions in parallel that are
-independent to each other.
+      # Compile C code using gcc
+      make jacobi-1d.gcc
+      # Run the GCC code
+      ./jacobi-1d.gcc
 
-.. _operation-chaining:
+   It should produce the same ``finish`` result as the SystemVerilog
+   simulation.
 
-Operation Chaining
-~~~~~~~~~~~~~~~~~~
+Running all benchmarks
+~~~~~~~~~~~~~~~~~~~~~~
 
-Operation chaining is an optimisation that can be added on to scheduling and allows for the
-sequential execution of instructions in a clock cycle, while executing other instructions in
-parallel in the same clock cycle.
+To run vericert on all benchmarks and simulate them all, one can use the
+base ``Makefile`` in addition to the
+``$VERICERT_ROOT/scripts/run-vericert.sh`` script.
 
-.. _if-conversion:
+.. code:: shell
 
-If-conversion
-~~~~~~~~~~~~~
+   # Build all the benchmarks using vericert, iverilog, verilator and GCC
+   cd $VERICERT_ROOT/benchmarks/polybench-syn
+   make
+   # Run all the simulations and compare against the GCC golden output
+   $VERICERT_ROOT/scripts/run-vericert.sh
 
-If-conversion is an optimisation which can turn code with simple control flow into a single block
-(called a hyper-block), using predicated instructions.
+This should produce a file containing the cycle counts for each
+benchmark, which can be viewed using:
 
-.. _functions:
+.. code:: shell
 
-Functions
-~~~~~~~~~
+   cat $VERICERT_ROOT/scripts/exec.csv
 
-Functions are currently only inlined in Vericert, however, we are working on a proper interface to
-integrate function calls into the hardware.
+Man Page
+========
 
-.. _coq-style-guide:
+.. raw:: org
 
-Coq Style Guide
----------------
+   #+transclude: [[file:man.org][file:man.org]] :exclude-elements "keyword" :level 2
 
-This style guide was taken from `Silveroak <https://github.com/project-oak/silveroak>`_, it outlines
-code style for Coq code in this repository. There are certainly other valid strategies and opinions
-on Coq code style; this is laid out purely in the name of consistency. For a visual example of the
-style, see the `example`_ at the bottom of this file.
+Unreleased Features
+===================
 
-.. _code-organization:
+The following are unreleased features in Vericert that are currently
+being worked on and have not been completely proven correct yet.
+Currently this includes features such as:
 
-Code organization
-~~~~~~~~~~~~~~~~~
+-  `scheduling <#scheduling>`__,
+-  `operation chaining <#operation-chaining>`__,
+-  `if-conversion <#if-conversion>`__, and
+-  `functions <#functions>`__.
 
-.. _legal-banner:
+This page gives some preliminary information on how the features are
+implemented and how the proofs for the features are being done. Once
+these features are properly implemented, they will be added to the
+proper documentation.
 
-Legal banner
-^^^^^^^^^^^^
+Scheduling
+----------
 
-- Files should begin with a copyright/license banner, as shown in the example above.
+.. raw:: org
 
-.. _import-statements:
+   #+cindex: scheduling
 
-Import statements
-^^^^^^^^^^^^^^^^^
+Scheduling is an optimisation which is used to run various instructions
+in parallel that are independent to each other.
 
-- ``Require Import`` statements should all go at the top of the file, followed by file-wide ``Import``
-  statements.
+Operation Chaining
+------------------
 
-  - =Import=s often contain notations or typeclass instances that might override notations or
-    instances from another library, so it’s nice to highlight them separately.
+Operation chaining is an optimisation that can be added on to scheduling
+and allows for the sequential execution of instructions in a clock
+cycle, while executing other instructions in parallel in the same clock
+cycle.
 
-- One ``Require Import`` statement per line; it’s easier to scan that way.
+If-conversion
+-------------
 
-- ``Require Import`` statements should use “fully-qualified” names (e.g. ``Require Import
-  Coq.ZArith.ZArith`` instead of ``Require Import ZArith``).
+If-conversion is an optimisation which can turn code with simple control
+flow into a single block (called a hyper-block), using predicated
+instructions.
 
-  - Use the ``Locate`` command to find the fully-qualified name!
+Functions
+---------
 
-- ``Require Import``’s should go in the following order:
+Functions are currently only inlined in Vericert, however, we are
+working on a proper interface to integrate function calls into the
+hardware.
 
-  1. Standard library dependencies (start with ``Coq.``)
+Scheduling proof
+================
 
-  2. External dependencies (anything outside the current project)
+Semantic identity properties
+----------------------------
 
-  3. Same-project dependencies
+This section corresponds to the proofs found in
+``src/hls/AbstrSemIdent.v``.
 
-- ``Require Import``’s with the same root library (the name before the first ``.``) should be
-  grouped together. Within each root-library group, they should be in alphabetical order (so
-  ``Coq.Lists.List`` before ``Coq.ZArith.ZArith``).
+``sem_merge_list``
+~~~~~~~~~~~~~~~~~~
 
-.. _notations-and-scopes:
+This lemma proves that given a forest ``f`` that executes from an
+initial context ``ctx`` to a state composed of ``rs``, ``ps`` and ``m``,
+that the evaluation of the merged arguments from the forest is
+equivalent to retrieving the arguments dynamically from the new state of
+the registers. This proves the correctness of the combination of
+``merge`` and ``list_translation`` to encode the list of arguments.
+
+One interesting note about this lemma is that it passes the latest state
+of the predicates from ``f`` into the function, i.e. ``forest_preds f``.
+This allows one to prove the theorem, however, using it later on is more
+problematic, as one cannot easily reuse it in the middle of an
+induction. Instead, one would have to prove that the future changes to
+the forest will not change the result of the current evaluation of the
+register arguments.
+
+It does make sense that this has to be proven somewhere, however, it's
+not clear if this results in the simplest proofs. However, one benefit
+is that this function already has to be used for the forward translation
+proof, so it can easily be reused for the backward execution proof.
+
+Backward proof
+--------------
 
-Notations and scopes
-^^^^^^^^^^^^^^^^^^^^
+This corresponds to the proof found in
+``src/hls/GiblePargenproofBackward.v``.
 
-- Any file-wide ``Local Open Scope``’s should come immediately after the =Import=s (see example).
+``abstr_seq_reverse_correct_fold``
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-  - Always use ``Local Open Scope``; just ``Open Scope`` will sneakily open the scope for those who
-    import your file.
+This proof is mainly tricky because one needs to infer concrete
+execution from the forest execution. There are also different forests
+that are each used for evaluation, for example, the final forest is used
+for predicate evaluation, whereas each individual forest is itself
+evaluated.
 
-- Put notations in their own separate modules or files, so that those who import your file can
-  choose whether or not they want the notations.
+However, the proof itself follows a very similar structure to the
+forward proof, with the addition of the assumption that the update
+produces an instruction that is evaluable. This assumption comes from
+the fact that the expression will still be in the forest at the end, or
+that it will be placed into the list of expressions that is checked for
+evaluation against the input instructions.
 
-  - Conflicting notations can cause a lot of headache, so it comes in very handy to leave this
-    flexibility!
+Coq Style Guide
+===============
 
-.. _formatting:
+This style guide was taken from
+`Silveroak <https://github.com/project-oak/silveroak>`__, it outlines
+code style for Coq code in this repository. There are certainly other
+valid strategies and opinions on Coq code style; this is laid out purely
+in the name of consistency. For a visual example of the style, see the
+`example <#example>`__ at the bottom of this file.
 
-Formatting
-~~~~~~~~~~
+Code organization
+-----------------
 
-.. _line-length:
+Legal banner
+~~~~~~~~~~~~
 
-Line length
-^^^^^^^^^^^
+-  Files should begin with a copyright/license banner, as shown in the
+   example above.
 
-- Maximum line length 80 characters.
+Import statements
+~~~~~~~~~~~~~~~~~
 
-  - Many Coq IDE setups divide the screen in half vertically and use only half to display source
-    code, so more than 80 characters can be genuinely hard to read on a laptop.
+-  ``Require Import`` statements should all go at the top of the file,
+   followed by file-wide ``Import`` statements.
 
-.. _whitespace-and-indentation:
+   -  =Import=s often contain notations or typeclass instances that
+      might override notations or instances from another library, so
+      it's nice to highlight them separately.
 
-Whitespace and indentation
-^^^^^^^^^^^^^^^^^^^^^^^^^^
+-  One ``Require Import`` statement per line; it's easier to scan that
+   way.
 
-- No trailing whitespace.
+-  ``Require Import`` statements should use "fully-qualified" names
+   (e.g. =Require Import Coq.ZArith.ZArith= instead of
+   ``Require Import ZArith``).
 
-- Spaces, not tabs.
+   -  Use the ``Locate`` command to find the fully-qualified name!
 
-- Files should end with a newline.
+-  ``Require Import``'s should go in the following order:
 
-  - Many editors do this automatically on save.
+   #. Standard library dependencies (start with ``Coq.``)
+   #. External dependencies (anything outside the current project)
+   #. Same-project dependencies
 
-- Colons may be either “English-spaced”, with no space before the colon and one space after (``x:
-  nat``) or “French-spaced”, with one space before and after (``x : nat``).
+-  ``Require Import``'s with the same root library (the name before the
+   first ``.``) should be grouped together. Within each root-library
+   group, they should be in alphabetical order (so ``Coq.Lists.List``
+   before ``Coq.ZArith.ZArith``).
 
-- Default indentation is 2 spaces.
+Notations and scopes
+~~~~~~~~~~~~~~~~~~~~
+
+-  Any file-wide ``Local Open Scope``'s should come immediately after
+   the =Import=s (see example).
 
-  - Keeping this small prevents complex proofs from being indented ridiculously far, and matches IDE
-    defaults.
+   -  Always use ``Local Open Scope``; just ``Open Scope`` will sneakily
+      open the scope for those who import your file.
 
-- Use 2-space indents if inserting a line break immediately after:
+-  Put notations in their own separate modules or files, so that those
+   who import your file can choose whether or not they want the
+   notations.
 
-  - ``Proof.``
+   -  Conflicting notations can cause a lot of headache, so it comes in
+      very handy to leave this flexibility!
 
-  - ``fun <...> =>``
+Formatting
+----------
 
-  - ``forall <...>,``
+Line length
+~~~~~~~~~~~
+
+-  Maximum line length 80 characters.
+
+   -  Many Coq IDE setups divide the screen in half vertically and use
+      only half to display source code, so more than 80 characters can
+      be genuinely hard to read on a laptop.
+
+Whitespace and indentation
+~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-  - ``exists <....>,``
+-  No trailing whitespace.
 
-- The style for indenting arguments in function application depends on where you make a line
-  break. If you make the line break immediately after the function name, use a 2-space
-  indent. However, if you make it after one or more arguments, align the next line with the first
-  argument:
+-  Spaces, not tabs.
 
-  .. code:: coq
+-  Files should end with a newline.
+
+   -  Many editors do this automatically on save.
+
+-  Colons may be either "English-spaced", with no space before the colon
+   and one space after (``x: nat``) or "French-spaced", with one space
+   before and after (``x : nat``).
+
+-  Default indentation is 2 spaces.
+
+   -  Keeping this small prevents complex proofs from being indented
+      ridiculously far, and matches IDE defaults.
+
+-  Use 2-space indents if inserting a line break immediately after:
+
+   -  ``Proof.``
+   -  ``fun <...> =>``
+   -  ``forall <...>,``
+   -  ``exists <....>,``
+
+-  The style for indenting arguments in function application depends on
+   where you make a line break. If you make the line break immediately
+   after the function name, use a 2-space indent. However, if you make
+   it after one or more arguments, align the next line with the first
+   argument:
+
+   .. code:: coq
 
       (Z.pow
          1 2)
       (Z.pow 1 2 3
              4 5 6)
 
-- ``Inductive`` cases should not be indented. Example:
+-  ``Inductive`` cases should not be indented. Example:
 
-  .. code:: coq
+   .. code:: coq
 
       Inductive Foo : Type :=
       | FooA : Foo
       | FooB : Foo
       .
 
-- ``match`` or ``lazymatch`` cases should line up with the “m” in ``match`` or “l” in ``lazymatch``,
-  as in the following examples:
+-  ``match`` or ``lazymatch`` cases should line up with the "m" in
+   ``match`` or "l" in ``lazymatch``, as in the following examples:
 
-  .. code:: coq
+   .. code:: coq
 
       match x with
       | 3 => true
@@ -321,25 +499,23 @@ Whitespace and indentation
            | |- context [eq] => idtac
            end.
 
-.. _definitions-and-fixpoints:
-
 Definitions and Fixpoints
-~~~~~~~~~~~~~~~~~~~~~~~~~
+-------------------------
 
-- It’s okay to leave the return type of ``Definition``’s and ``Fixpoint``’s implicit
-  (e.g. ``Definition x := 5`` instead of ``Definition x : nat := 5``) when the type is very simple
-  or obvious (for instance, the definition is in a file which deals exclusively with operations on
-  ``Z``).
-
-.. _inductives:
+-  It's okay to leave the return type of ``Definition``'s and
+   ``Fixpoint``'s implicit (e.g. ``Definition x := 5`` instead of
+   ``Definition x : nat := 5``) when the type is very simple or obvious
+   (for instance, the definition is in a file which deals exclusively
+   with operations on ``Z``).
 
 Inductives
-~~~~~~~~~~
+----------
 
-- The ``.`` ending an ``Inductive`` can be either on the same line as the last case or on its own
-  line immediately below. That is, both of the following are acceptable:
+-  The ``.`` ending an ``Inductive`` can be either on the same line as
+   the last case or on its own line immediately below. That is, both of
+   the following are acceptable:
 
-  .. code:: coq
+   .. code:: coq
 
       Inductive Foo : Type :=
       | FooA : Foo
@@ -349,75 +525,80 @@ Inductives
       | FooA : Foo
       | FooB : Foo.
 
-.. _lemmatheorem-statements:
-
 Lemma/Theorem statements
-~~~~~~~~~~~~~~~~~~~~~~~~
-
-- Generally, use ``Theorem`` for the most important, top-level facts you prove and ``Lemma`` for
-  everything else.
-
-- Insert a line break after the colon in the lemma statement.
-
-- Insert a line break after the comma for ``forall`` or ``exist`` quantifiers.
-
-- Implication arrows (``->``) should share a line with the previous hypothesis, not the following
-  one.
-
-- There is no need to make a line break after every ``->``; short preconditions may share a line.
-
-.. _proofs-and-tactics:
+------------------------
+
+-  Generally, use ``Theorem`` for the most important, top-level facts
+   you prove and ``Lemma`` for everything else.
+-  Insert a line break after the colon in the lemma statement.
+-  Insert a line break after the comma for ``forall`` or ``exist``
+   quantifiers.
+-  Implication arrows (``->``) should share a line with the previous
+   hypothesis, not the following one.
+-  There is no need to make a line break after every ``->``; short
+   preconditions may share a line.
 
 Proofs and tactics
-~~~~~~~~~~~~~~~~~~
-
-- Use the ``Proof`` command (lined up vertically with ``Lemma`` or ``Theorem`` it corresponds to) to
-  open a proof, and indent the first line after it 2 spaces.
+------------------
 
-- Very small proofs (where ``Proof. <tactics> Qed.`` is <= 80 characters) can go all in one line.
+-  Use the ``Proof`` command (lined up vertically with ``Lemma`` or
+   ``Theorem`` it corresponds to) to open a proof, and indent the first
+   line after it 2 spaces.
 
-- When ending a proof, align the ending statement (``Qed``, ``Admitted``, etc.) with ``Proof``.
+-  Very small proofs (where ``Proof. <tactics> Qed.`` is <= 80
+   characters) can go all in one line.
 
-- Avoid referring to autogenerated names (e.g. ``H0``, ``n0``). It’s okay to let Coq generate these
-  names, but you should not explicitly refer to them in your proof. So ``intros; my_solver`` is
-  fine, but ``intros; apply H1; my_solver`` is not fine.
+-  When ending a proof, align the ending statement (``Qed``,
+   ``Admitted``, etc.) with ``Proof``.
 
-  - You can force a non-autogenerated name by either putting the variable before the colon in the
-    lemma statement (``Lemma foo x : ...`` instead of ``Lemma foo : forall x, ...``), or by passing
-    arguments to ``intros`` (e.g. ``intros ? x`` to name the second argument ``x``)
+-  Avoid referring to autogenerated names (e.g. =H0=, ``n0``). It's okay
+   to let Coq generate these names, but you should not explicitly refer
+   to them in your proof. So ``intros; my_solver`` is fine, but
+   ``intros; apply H1; my_solver`` is not fine.
 
-- This way, the proof won’t break when new hypotheses are added or autogenerated variable names
-  change.
+   -  You can force a non-autogenerated name by either putting the
+      variable before the colon in the lemma statement
+      (``Lemma foo x : ...`` instead of ``Lemma foo : forall x, ...``),
+      or by passing arguments to ``intros`` (e.g. =intros ? x= to name
+      the second argument ``x``)
 
-- Use curly braces ``{}`` for subgoals, instead of bullets.
+-  This way, the proof won't break when new hypotheses are added or
+   autogenerated variable names change.
 
-- *Never write tactics with more than one subgoal focused.* This can make the proof very confusing
-  to step through! If you have more than one subgoal, use curly braces.
+-  Use curly braces ``{}`` for subgoals, instead of bullets.
 
-- Consider adding a comment after the opening curly brace that explains what case you’re in (see
-  example).
+-  *Never write tactics with more than one subgoal focused.* This can
+   make the proof very confusing to step through! If you have more than
+   one subgoal, use curly braces.
 
-  - This is not necessary for small subgoals but can help show the major lines of reasoning in large
-    proofs.
+-  Consider adding a comment after the opening curly brace that explains
+   what case you're in (see example).
 
-- If invoking a tactic that is expected to return multiple subgoals, use ``[ | ... | ]`` before the
-  ``.`` to explicitly specify how many subgoals you expect.
+   -  This is not necessary for small subgoals but can help show the
+      major lines of reasoning in large proofs.
 
-  - Examples: ``split; [ | ].`` ``induction z; [ | | ].``
+-  If invoking a tactic that is expected to return multiple subgoals,
+   use ``[ | ... | ]`` before the ``.`` to explicitly specify how many
+   subgoals you expect.
 
-  - This helps make code more maintainable, because it fails immediately if your tactic no longer
-    solves as many subgoals as expected (or unexpectedly solves more).
+   -  Examples: ``split; [ | ].`` ``induction z; [ | | ].``
+   -  This helps make code more maintainable, because it fails
+      immediately if your tactic no longer solves as many subgoals as
+      expected (or unexpectedly solves more).
 
-- If invoking a string of tactics (composed by ``;``) that will break the goal into multiple
-  subgoals and then solve all but one, still use ``[ ]`` to enforce that all but one goal is solved.
+-  If invoking a string of tactics (composed by ``;``) that will break
+   the goal into multiple subgoals and then solve all but one, still use
+   ``[ ]`` to enforce that all but one goal is solved.
 
-  - Example: ``split; try lia; [ ]``.
+   -  Example: ``split; try lia; [ ]``.
 
-- Tactics that consist only of ``repeat``-ing a procedure (e.g. ``repeat match``, ``repeat first``)
-  should factor out a single step of that procedure a separate tactic called ``<tactic name>_step``,
-  because the single-step version is much easier to debug. For instance:
+-  Tactics that consist only of ``repeat``-ing a procedure (e.g.
+   ``repeat match``, ``repeat first``) should factor out a single step
+   of that procedure a separate tactic called ``<tactic name>_step``,
+   because the single-step version is much easier to debug. For
+   instance:
 
-  .. code:: coq
+   .. code:: coq
 
       Ltac crush_step :=
         match goal with
@@ -426,101 +607,111 @@ Proofs and tactics
         end.
       Ltac crush := repeat crush_step.
 
-.. _naming:
-
 Naming
-~~~~~~
-
-- Helper proofs about standard library datatypes should go in a module that is named to match the
-  standard library module (see example).
+------
 
-  - This makes the helper proofs look like standard-library ones, which is helpful for categorizing
-    them if they’re genuinely at the standard-library level of abstraction.
+-  Helper proofs about standard library datatypes should go in a module
+   that is named to match the standard library module (see example).
 
-- Names of modules should start with capital letters.
+   -  This makes the helper proofs look like standard-library ones,
+      which is helpful for categorizing them if they're genuinely at the
+      standard-library level of abstraction.
 
-- Names of inductives and their constructors should start with capital letters.
+-  Names of modules should start with capital letters.
 
-- Names of other definitions/lemmas should be snake case.
+-  Names of inductives and their constructors should start with capital
+   letters.
 
-.. _example:
+-  Names of other definitions/lemmas should be snake case.
 
 Example
-~~~~~~~
+-------
 
 A small standalone Coq file that exhibits many of the style points.
 
-.. coq:: no-out
-
-    (*
-     * Vericert: Verified high-level synthesis.
-     * Copyright (C) 2021 Name <email@example.com>
-     *
-     * <License...>
-     *)
-
-      Require Import Coq.Lists.List.
-      Require Import Coq.micromega.Lia.
-      Require Import Coq.ZArith.ZArith.
-      Import ListNotations.
-      Local Open Scope Z_scope.
-
-      (* Helper proofs about standard library integers (Z) go within [Module Z] so
-         that they match standard-library Z lemmas when used. *)
-      Module Z.
-        Lemma pow_3_r x : x ^ 3 = x * x * x.
-        Proof. lia. Qed. (* very short proofs can go all on one line *)
-
-        Lemma pow_4_r x : x ^ 4 = x * x * x * x.
-        Proof.
-          change 4 with (Z.succ (Z.succ (Z.succ (Z.succ 0)))).
-          repeat match goal with
-                 | _ => rewrite Z.pow_1_r
-                 | _ => rewrite Z.pow_succ_r by lia
-                 | |- context [x * (?a * ?b)] =>
-                   replace (x * (a * b)) with (a * b * x) by lia
-                 | _ => reflexivity
-                 end.
-        Qed.
-      End Z.
-      (* Now we can access the lemmas above as Z.pow_3_r and Z.pow_4_r, as if they
-         were in the ZArith library! *)
-
-      Definition bar (x y : Z) := x ^ (y + 1).
-
-      (* example with a painfully manual proof to show case formatting *)
-      Lemma bar_upper_bound :
-        forall x y a,
-          0 <= x <= a -> 0 <= y ->
-          0 <= bar x y <= a ^ (y + 1).
-      Proof.
-        (* avoid referencing autogenerated names by explicitly naming variables *)
-        intros x y a Hx Hy. revert y Hy x a Hx.
-        (* explicitly indicate # subgoals with [ | ... | ] if > 1 *)
-        cbv [bar]; refine (natlike_ind _ _ _); [ | ].
-        { (* y = 0 *)
-          intros; lia. }
-        { (* y = Z.succ _ *)
-          intros.
-          rewrite Z.add_succ_l, Z.pow_succ_r by lia.
-          split.
-          { (* 0 <= bar x y *)
-            apply Z.mul_nonneg_nonneg; [ lia | ].
-            apply Z.pow_nonneg; lia. }
-          { (* bar x y < a ^ y *)
-            rewrite Z.pow_succ_r by lia.
-            apply Z.mul_le_mono_nonneg; try lia;
-              [ apply Z.pow_nonneg; lia | ].
-            (* For more flexible proofs, use match statements to find hypotheses
-               rather than referring to them by autogenerated names like H0. In this
-               case, we'll take any hypothesis that applies to and then solves the
-               goal. *)
-            match goal with H : _ |- _ => apply H; solve [auto] end. } }
-      Qed.
-
-      (* Put notations in a separate module or file so that importers can
-         decide whether or not to use them. *)
-      Module BarNotations.
-        Infix "#" := bar (at level 40) : Z_scope.
-        Notation "x '##'" := (bar x x) (at level 40) : Z_scope.
-      End BarNotations.
+.. code:: coq
+
+   (*
+    * Vericert: Verified high-level synthesis.
+    * Copyright (C) 2021 Name <email@example.com>
+    *
+    * <License...>
+    *)
+
+     Require Import Coq.Lists.List.
+     Require Import Coq.micromega.Lia.
+     Require Import Coq.ZArith.ZArith.
+     Import ListNotations.
+     Local Open Scope Z_scope.
+
+     (* Helper proofs about standard library integers (Z) go within [Module Z] so
+        that they match standard-library Z lemmas when used. *)
+     Module Z.
+       Lemma pow_3_r x : x ^ 3 = x * x * x.
+       Proof. lia. Qed. (* very short proofs can go all on one line *)
+
+       Lemma pow_4_r x : x ^ 4 = x * x * x * x.
+       Proof.
+         change 4 with (Z.succ (Z.succ (Z.succ (Z.succ 0)))).
+         repeat match goal with
+                | _ => rewrite Z.pow_1_r
+                | _ => rewrite Z.pow_succ_r by lia
+                | |- context [x * (?a * ?b)] =>
+                  replace (x * (a * b)) with (a * b * x) by lia
+                | _ => reflexivity
+                end.
+       Qed.
+     End Z.
+     (* Now we can access the lemmas above as Z.pow_3_r and Z.pow_4_r, as if they
+        were in the ZArith library! *)
+
+     Definition bar (x y : Z) := x ^ (y + 1).
+
+     (* example with a painfully manual proof to show case formatting *)
+     Lemma bar_upper_bound :
+       forall x y a,
+         0 <= x <= a -> 0 <= y ->
+         0 <= bar x y <= a ^ (y + 1).
+     Proof.
+       (* avoid referencing autogenerated names by explicitly naming variables *)
+       intros x y a Hx Hy. revert y Hy x a Hx.
+       (* explicitly indicate # subgoals with [ | ... | ] if > 1 *)
+       cbv [bar]; refine (natlike_ind _ _ _); [ | ].
+       { (* y = 0 *)
+         intros; lia. }
+       { (* y = Z.succ _ *)
+         intros.
+         rewrite Z.add_succ_l, Z.pow_succ_r by lia.
+         split.
+         { (* 0 <= bar x y *)
+           apply Z.mul_nonneg_nonneg; [ lia | ].
+           apply Z.pow_nonneg; lia. }
+         { (* bar x y < a ^ y *)
+           rewrite Z.pow_succ_r by lia.
+           apply Z.mul_le_mono_nonneg; try lia;
+             [ apply Z.pow_nonneg; lia | ].
+           (* For more flexible proofs, use match statements to find hypotheses
+              rather than referring to them by autogenerated names like H0. In this
+              case, we'll take any hypothesis that applies to and then solves the
+              goal. *)
+           match goal with H : _ |- _ => apply H; solve [auto] end. } }
+     Qed.
+
+     (* Put notations in a separate module or file so that importers can
+        decide whether or not to use them. *)
+     Module BarNotations.
+       Infix "#" := bar (at level 40) : Z_scope.
+       Notation "x '##'" := (bar x x) (at level 40) : Z_scope.
+     End BarNotations.
+
+.. _cindex:
+
+Index - Features
+================
+
+GNU Free Documentation License
+==============================
+
+.. raw:: org
+
+   #+include: res/fdl.org