23 files changed, 854 insertions, 93 deletions
diff --git a/.gitignore b/.gitignore
index 6568d8d..5574171 100644
--- a/.gitignore
+++ b/.gitignore
@@ -83,9 +83,7 @@ obj_dir/
 
 creduce_bug_*/
 
-/docs/man/
-/docs/manual/
-/docs/src/
+/doc/src/
 /html/
 
 *~
diff --git a/Makefile b/Makefile
index a6aa914..3128c23 100644
--- a/Makefile
+++ b/Makefile
@@ -17,7 +17,8 @@ COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source
 COQMAKE := $(COQBIN)coq_makefile
 
 COQDOCFLAGS := --no-lib-name -l
-ALECTRYON_OPTS := --html-minification --long-line-threshold 80 --coq-driver sertop_noexec $(COQINCLUDES)
+ALECTRYON_OPTS := --no-header --html-minification --long-line-threshold 80 \
+                  --coq-driver sertop_noexec $(COQINCLUDES)
 
 VS := src/Compiler.v src/Simulator.v src/HLSOpts.v $(foreach d, common hls bourdoncle, $(wildcard src/$(d)/*.v))
 LIT := docs/basic-block-generation.org docs/scheduler.org docs/scheduler-languages.org
diff --git a/doc/Makefile b/doc/Makefile
new file mode 100644
index 0000000..5662645
--- /dev/null
+++ b/doc/Makefile
@@ -0,0 +1,24 @@
+# Minimal makefile for Sphinx documentation
+#
+
+# You can set these variables from the command line, and also
+# from the environment for the first two.
+SPHINXOPTS        ?=
+SPHINXBUILD       ?= sphinx-build
+SOURCEDIR         = .
+BUILDDIR          = _build
+SOURCE_DATE_EPOCH = $(shell git log -1 --format=%ct)
+
+VS_DOCS := ../src/Compiler.v ../src/hls/RTLBlockInstr.v
+
+# Put it first so that "make" without argument is like "make help".
+help:
+	@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
+
+.PHONY: help Makefile
+
+# Catch-all target: route all unknown targets to Sphinx using the new
+# "make mode" option.  $(O) is meant as a shortcut for $(SPHINXOPTS).
+%: Makefile
+	$(foreach d,$(VS_DOCS),cp $(d) $(patsubst ../%,%,$(d));)
+	@$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
diff --git a/docs/Makefile b/doc/Makefile.extr
index 9d4f361..9d4f361 100644
--- a/docs/Makefile
+++ b/doc/Makefile.extr
diff --git a/docs/README.org b/doc/README.org
index 4113ed9..4113ed9 100644
--- a/docs/README.org
+++ b/doc/README.org
diff --git a/doc/_static/css/custom.css b/doc/_static/css/custom.css
new file mode 100644
index 0000000..66a1e35
--- /dev/null
+++ b/doc/_static/css/custom.css
@@ -0,0 +1,11 @@
+.alectryon-coqdoc .doc .code,
+.alectryon-coqdoc .doc .comment,
+.alectryon-coqdoc .doc .inlinecode,
+.alectryon-mref,
+.alectryon-block, .alectryon-io,
+.alectryon-toggle-label, .alectryon-banner, pre, tt, code {
+    font-family: 'Iosevka Fixed Slab', 'Iosevka Slab Web', 'Iosevka Web', 'Iosevka Slab',
+                 'Iosevka', 'Fira Code', monospace;
+    font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */;
+    line-height: initial;
+}
diff --git a/docs/images/toolflow.pdf b/doc/_static/images/toolflow.pdf
index 5fcee67..5fcee67 100644
--- a/docs/images/toolflow.pdf
+++ b/doc/_static/images/toolflow.pdf
diff --git a/docs/images/toolflow.png b/doc/_static/images/toolflow.png
index 601d6be..601d6be 100644
--- a/docs/images/toolflow.png
+++ b/doc/_static/images/toolflow.png
diff --git a/docs/images/toolflow.svg b/doc/_static/images/toolflow.svg
index 0d8f39f..0d8f39f 100644
--- a/docs/images/toolflow.svg
+++ b/doc/_static/images/toolflow.svg
diff --git a/docs/common.org b/doc/common.org
index aa27264..aa27264 100644
--- a/docs/common.org
+++ b/doc/common.org
diff --git a/doc/conf.py b/doc/conf.py
new file mode 100644
index 0000000..015f030
--- /dev/null
+++ b/doc/conf.py
@@ -0,0 +1,85 @@
+# Configuration file for the Sphinx documentation builder.
+#
+# This file only contains a selection of the most common options. For a full
+# list see the documentation:
+# https://www.sphinx-doc.org/en/master/usage/configuration.html
+
+# -- Path setup --------------------------------------------------------------
+
+# If extensions (or modules to document with autodoc) are in another directory,
+# add these directories to sys.path here. If the directory is relative to the
+# documentation root, use os.path.abspath to make it absolute, like shown here.
+#
+# import os
+# import sys
+# sys.path.insert(0, os.path.abspath('.'))
+
+
+# -- Project information -----------------------------------------------------
+
+project = 'Vericert'
+copyright = '2022  Yann Herklotz, John Wickerson'
+author = 'Yann Herklotz, John Wickerson'
+
+# The full version, including alpha/beta/rc tags
+release = 'v1.2.2'
+
+
+# -- General configuration ---------------------------------------------------
+
+# Add any Sphinx extension module names here, as strings. They can be
+# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
+# ones.
+extensions = [ "alectryon.sphinx" ]
+
+# Add any paths that contain templates here, relative to this directory.
+templates_path = ['_templates']
+
+# List of patterns, relative to source directory, that match files and
+# directories to ignore when looking for source files.
+# This pattern also affects html_static_path and html_extra_path.
+exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store']
+
+pygments_style = "emacs"
+
+
+# -- Options for HTML output -------------------------------------------------
+
+# The theme to use for HTML and HTML Help pages.  See the documentation for
+# a list of builtin themes.
+#
+html_theme = 'alabaster'
+
+# Add any paths that contain custom static files (such as style sheets) here,
+# relative to this directory. They are copied after the builtin static files,
+# so a file named "default.css" will overwrite the builtin "default.css".
+html_static_path = ['_static']
+
+html_css_files = [
+    'css/custom.css',
+]
+
+
+# -- LaTeX configuration -----------------------------------------------------
+
+latex_engine = "xelatex"
+
+
+# -- Alectryon configuration -------------------------------------------------
+
+import alectryon.docutils
+alectryon.docutils.CACHE_DIRECTORY = "_build/alectryon/"
+alectryon.docutils.LONG_LINE_THRESHOLD = 80
+
+alectryon.docutils.AlectryonTransform.DRIVER_ARGS["sertop"] = [
+    "-R" "../src,vericert",
+    "-R" "../lib/CompCert/lib,compcert.lib",
+    "-R" "../lib/CompCert/common,compcert.common",
+    "-R" "../lib/CompCert/verilog,compcert.verilog",
+    "-R" "../lib/CompCert/backend,compcert.backend",
+    "-R" "../lib/CompCert/cfrontend,compcert.cfrontend",
+    "-R" "../lib/CompCert/driver,compcert.driver",
+    "-R" "../lib/CompCert/cparser,compcert.cparser",
+    "-R" "../lib/CompCert/flocq,Flocq",
+    "-R" "../lib/CompCert/MenhirLib,MenhirLib"
+]
diff --git a/docs/documentation.org b/doc/documentation.org
index 85bc8fd..85bc8fd 100644
--- a/docs/documentation.org
+++ b/doc/documentation.org
diff --git a/doc/docutils.conf b/doc/docutils.conf
new file mode 100644
index 0000000..1bf4d83
--- /dev/null
+++ b/doc/docutils.conf
@@ -0,0 +1,2 @@
+[restructuredtext parser]
+syntax_highlight = short
diff --git a/doc/index.rst b/doc/index.rst
new file mode 100644
index 0000000..ebb99df
--- /dev/null
+++ b/doc/index.rst
@@ -0,0 +1,26 @@
+.. Vericert documentation master file, created by
+   sphinx-quickstart on Sat Mar 26 18:15:40 2022.
+   You can adapt this file completely to your liking, but it should at least
+   contain the root `toctree` directive.
+
+Vericert's Documentation
+========================
+
+.. toctree::
+   :maxdepth: 2
+   :caption: Content:
+
+   vericert
+
+.. toctree::
+   :maxdepth: 1
+   :caption: Sources:
+
+   src/Compiler
+   src/hls/RTLBlockInstr
+
+Indices
+==================
+
+* :ref:`genindex`
+* :ref:`search`
diff --git a/doc/make.bat b/doc/make.bat
new file mode 100644
index 0000000..153be5e
--- /dev/null
+++ b/doc/make.bat
@@ -0,0 +1,35 @@
+@ECHO OFF
+
+pushd %~dp0
+
+REM Command file for Sphinx documentation
+
+if "%SPHINXBUILD%" == "" (
+	set SPHINXBUILD=sphinx-build
+)
+set SOURCEDIR=.
+set BUILDDIR=_build
+
+if "%1" == "" goto help
+
+%SPHINXBUILD% >NUL 2>NUL
+if errorlevel 9009 (
+	echo.
+	echo.The 'sphinx-build' command was not found. Make sure you have Sphinx
+	echo.installed, then set the SPHINXBUILD environment variable to point
+	echo.to the full path of the 'sphinx-build' executable. Alternatively you
+	echo.may add the Sphinx directory to PATH.
+	echo.
+	echo.If you don't have Sphinx installed, grab it from
+	echo.https://www.sphinx-doc.org/
+	exit /b 1
+)
+
+%SPHINXBUILD% -M %1 %SOURCEDIR% %BUILDDIR% %SPHINXOPTS% %O%
+goto end
+
+:help
+%SPHINXBUILD% -M help %SOURCEDIR% %BUILDDIR% %SPHINXOPTS% %O%
+
+:end
+popd
diff --git a/docs/man.org b/doc/man.org
index cb6143f..cb6143f 100644
--- a/docs/man.org
+++ b/doc/man.org
diff --git a/docs/res/coqdoc.css b/doc/res/coqdoc.css
index 5572aaa..5572aaa 100644
--- a/docs/res/coqdoc.css
+++ b/doc/res/coqdoc.css
diff --git a/docs/res/fdl.org b/doc/res/fdl.org
index 81e2cd9..81e2cd9 100644
--- a/docs/res/fdl.org
+++ b/doc/res/fdl.org
diff --git a/docs/res/install-deps.el b/doc/res/install-deps.el
index 09cf4ae..09cf4ae 100644
--- a/docs/res/install-deps.el
+++ b/doc/res/install-deps.el
diff --git a/docs/res/publish.el b/doc/res/publish.el
index c083eb0..c083eb0 100644
--- a/docs/res/publish.el
+++ b/doc/res/publish.el
diff --git a/doc/vericert.rst b/doc/vericert.rst
new file mode 100644
index 0000000..3c8eaeb
--- /dev/null
+++ b/doc/vericert.rst
@@ -0,0 +1,530 @@
+===============
+Vericert Manual
+===============
+
+
+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).
+
+.. _fig:design:
+
+.. figure:: /_static/images/toolflow.png
+
+    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.
+
+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.
+
+.. index:: vericert
+
+.. _building:
+
+Building Vericert
+-----------------
+
+
+Testing
+~~~~~~~
+
+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
+
+Or by running the test suite using the following command:
+
+.. code:: shell
+
+    make test
+
+.. _using-vericert:
+
+.. index:: vericert
+
+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.
+
+.. code:: shell
+
+    vericert main.c -o main.v
+
+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:
+
+.. code:: shell
+
+    iverilog -o main_v main.v
+
+When executing, it should therefore print the following:
+
+.. code:: shell
+
+    $ ./main_v
+    finished: 50
+
+This gives the same result as executing the C in the following way:
+
+.. code:: shell
+
+    $ gcc -o main_c main.c
+    $ ./main_c
+    $ echo $?
+    50
+
+Man pages
+~~~~~~~~~
+
+.. _unreleased-features:
+
+Unreleased Features
+-------------------
+
+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:
+
+- `scheduling`_,
+
+- `operation-chaining`_,
+
+- `if-conversion`_, and
+
+- `functions`_.
+
+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.
+
+.. _scheduling:
+
+Scheduling
+~~~~~~~~~~
+
+Scheduling is an optimisation which is used to run various instructions in parallel that are
+independent to each other.
+
+.. _operation-chaining:
+
+Operation Chaining
+~~~~~~~~~~~~~~~~~~
+
+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.
+
+.. _if-conversion:
+
+If-conversion
+~~~~~~~~~~~~~
+
+If-conversion is an optimisation which can turn code with simple control flow into a single block
+(called a hyper-block), using predicated instructions.
+
+.. _functions:
+
+Functions
+~~~~~~~~~
+
+Functions are currently only inlined in Vericert, however, we are working on a proper interface to
+integrate function calls into the hardware.
+
+.. _coq-style-guide:
+
+Coq Style Guide
+---------------
+
+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.
+
+.. _code-organization:
+
+Code organization
+~~~~~~~~~~~~~~~~~
+
+.. _legal-banner:
+
+Legal banner
+^^^^^^^^^^^^
+
+- Files should begin with a copyright/license banner, as shown in the example above.
+
+.. _import-statements:
+
+Import statements
+^^^^^^^^^^^^^^^^^
+
+- ``Require Import`` statements should all go at the top of the file, followed by file-wide ``Import``
+  statements.
+
+  - =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.
+
+- One ``Require Import`` statement per line; it’s easier to scan that way.
+
+- ``Require Import`` statements should use “fully-qualified” names (e.g. ``Require Import
+  Coq.ZArith.ZArith`` instead of ``Require Import ZArith``).
+
+  - Use the ``Locate`` command to find the fully-qualified name!
+
+- ``Require Import``’s should go in the following order:
+
+  1. Standard library dependencies (start with ``Coq.``)
+
+  2. External dependencies (anything outside the current project)
+
+  3. Same-project dependencies
+
+- ``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``).
+
+.. _notations-and-scopes:
+
+Notations and scopes
+^^^^^^^^^^^^^^^^^^^^
+
+- Any file-wide ``Local Open Scope``’s should come immediately after the =Import=s (see example).
+
+  - Always use ``Local Open Scope``; just ``Open Scope`` will sneakily open the scope for those who
+    import your file.
+
+- 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.
+
+  - Conflicting notations can cause a lot of headache, so it comes in very handy to leave this
+    flexibility!
+
+.. _formatting:
+
+Formatting
+~~~~~~~~~~
+
+.. _line-length:
+
+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:
+
+Whitespace and indentation
+^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+- No trailing whitespace.
+
+- Spaces, not tabs.
+
+- 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:
+
+  .. 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:
+
+  .. code:: coq
+
+      match x with
+      | 3 => true
+      | _ => false
+      end.
+
+      lazymatch x with
+      | 3 => idtac
+      | _ => fail "Not equal to 3:" x
+      end.
+
+      repeat match goal with
+             | _ => progress subst
+             | _ => reflexivity
+             end.
+
+      do 2 lazymatch goal with
+           | |- 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:
+
+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:
+
+  .. code:: coq
+
+      Inductive Foo : Type :=
+      | FooA : Foo
+      | FooB : Foo
+      .
+      Inductive Foo : Type :=
+      | 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:
+
+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.
+
+- When ending a proof, align the ending statement (``Qed``, ``Admitted``, etc.) with ``Proof``.
+
+- 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.
+
+  - 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``)
+
+- This way, the proof won’t break when new hypotheses are added or autogenerated variable names
+  change.
+
+- Use curly braces ``{}`` for subgoals, instead of bullets.
+
+- *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.
+
+- Consider adding a comment after the opening curly brace that explains what case you’re in (see
+  example).
+
+  - This is not necessary for small subgoals but can help show the major lines of reasoning in large
+    proofs.
+
+- If invoking a tactic that is expected to return multiple subgoals, use ``[ | ... | ]`` before the
+  ``.`` to explicitly specify how many subgoals you expect.
+
+  - 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.
+
+  - 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:
+
+  .. code:: coq
+
+      Ltac crush_step :=
+        match goal with
+        | _ => progress subst
+        | _ => reflexivity
+        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.
+
+- Names of modules should start with capital letters.
+
+- Names of inductives and their constructors should start with capital letters.
+
+- Names of other definitions/lemmas should be snake case.
+
+.. _example:
+
+Example
+~~~~~~~
+
+A small standalone Coq file that exhibits many of the style points.
+
+.. 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.
diff --git a/src/Compiler.v b/src/Compiler.v
index cd05aa9..d6d87e2 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -1,22 +1,21 @@
-(*
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
- *
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as published by
- * the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with this program.  If not, see <https://www.gnu.org/licenses/>.
- *)
-
 (*|
+..
+   Vericert: Verified high-level synthesis.
+   Copyright (C) 2019-2022 Yann Herklotz <yann@yannherklotz.com>
+
+   This program is free software: you can redistribute it and/or modify
+   it under the terms of the GNU General Public License as published by
+   the Free Software Foundation, either version 3 of the License, or
+   (at your option) any later version.
+
+   This program is distributed in the hope that it will be useful,
+   but WITHOUT ANY WARRANTY; without even the implied warranty of
+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+   GNU General Public License for more details.
+
+   You should have received a copy of the GNU General Public License
+   along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
 ==============
 Compiler Proof
 ==============
@@ -27,9 +26,12 @@ backwards simulation correct.
 Imports
 =======
 
+
 We first need to import all of the modules that are used in the correctness
 proof, which includes all of the passes that are performed in Vericert and the
 CompCert front end.
+
+.. coq:: none
 |*)
 
 Require compcert.backend.Selection.
@@ -133,24 +135,28 @@ Definition partial_if {A: Type}
 
 Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.
 
-Definition match_if {A: Type} (flag: unit -> bool) (R: A -> A -> Prop): A -> A -> Prop :=
+Definition match_if {A: Type} (flag: unit -> bool) (R: A -> A -> Prop)
+  : A -> A -> Prop :=
   if flag tt then R else eq.
 
 Lemma total_if_match:
-  forall (A: Type) (flag: unit -> bool) (f: A -> A) (rel: A -> A -> Prop) (prog: A),
-  (forall p, rel p (f p)) ->
+  forall (A: Type) (flag: unit -> bool) (f: A -> A)
+         (rel: A -> A -> Prop) (prog: A),
+    (forall p, rel p (f p)) ->
   match_if flag rel prog (total_if flag f prog).
 Proof.
   intros. unfold match_if, total_if. destruct (flag tt); auto.
 Qed.
 
 Lemma partial_if_match:
-  forall (A: Type) (flag: unit -> bool) (f: A -> res A) (rel: A -> A -> Prop) (prog tprog: A),
+  forall (A: Type) (flag: unit -> bool) (f: A -> res A)
+         (rel: A -> A -> Prop) (prog tprog: A),
   (forall p tp, f p = OK tp -> rel p tp) ->
   partial_if flag f prog = OK tprog ->
   match_if flag rel prog tprog.
 Proof.
-  intros. unfold match_if, partial_if in *. destruct (flag tt). auto. congruence.
+  intros. unfold match_if, partial_if in *. destruct (flag tt).
+  auto. congruence.
 Qed.
 
 Remark forward_simulation_identity:
@@ -164,12 +170,14 @@ Proof.
 Qed.
 
 Lemma match_if_simulation:
-  forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (transf: A -> A -> Prop) (prog tprog: A),
+  forall (A: Type) (sem: A -> semantics) (flag: unit -> bool)
+         (transf: A -> A -> Prop) (prog tprog: A),
   match_if flag transf prog tprog ->
   (forall p tp, transf p tp -> forward_simulation (sem p) (sem tp)) ->
   forward_simulation (sem prog) (sem tprog).
 Proof.
-  intros. unfold match_if in *. destruct (flag tt). eauto. subst. apply forward_simulation_identity.
+  intros. unfold match_if in *. destruct (flag tt). eauto. subst.
+  apply forward_simulation_identity.
 Qed.
 
 (*|
@@ -188,13 +196,16 @@ Definition transf_backend (r : RTL.program) : res Verilog.program :=
    @@ print (print_RTL 1)
    @@ Renumber.transf_program
    @@ print (print_RTL 2)
-   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
+   @@ total_if Compopts.optim_constprop
+      (time "Constant propagation" Constprop.transf_program)
    @@ print (print_RTL 3)
-   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
+   @@ total_if Compopts.optim_constprop
+      (time "Renumbering" Renumber.transf_program)
    @@ print (print_RTL 4)
   @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
    @@ print (print_RTL 5)
-  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
+  @@@ partial_if Compopts.optim_redundancy
+      (time "Redundancy elimination" Deadcode.transf_program)
    @@ print (print_RTL 6)
   @@@ time "Unused globals" Unusedglob.transform_program
    @@ print (print_RTL 7)
@@ -220,8 +231,10 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_RTL 0)
   @@@ transf_backend.
 
-(* This is an unverified version of transf_hls with some experimental additions such as scheduling
-that aren't completed yet. *)
+(*|
+This is an unverified version of transf_hls with some experimental additions
+such as scheduling that aren't completed yet.
+|*)
 Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
   OK p
   @@@ SimplExpr.transl_program
@@ -234,13 +247,16 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_RTL 1)
    @@ Renumber.transf_program
    @@ print (print_RTL 2)
-   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
+   @@ total_if Compopts.optim_constprop
+      (time "Constant propagation" Constprop.transf_program)
    @@ print (print_RTL 3)
-   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
+   @@ total_if Compopts.optim_constprop
+      (time "Renumbering" Renumber.transf_program)
    @@ print (print_RTL 4)
   @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
    @@ print (print_RTL 5)
-  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
+  @@@ partial_if Compopts.optim_redundancy
+      (time "Redundancy elimination" Deadcode.transf_program)
    @@ print (print_RTL 6)
   @@@ time "Unused globals" Unusedglob.transform_program
    @@ print (print_RTL 7)
@@ -280,7 +296,8 @@ Definition CompCert's_passes :=
   ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog)
   ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog)
   ::: mkpass Unusedglobproof.match_prog
-  ::: (@mkpass _ _ HTLgenproof.match_prog (HTLgenproof.TransfHTLLink HTLgen.transl_program))
+  ::: (@mkpass _ _ HTLgenproof.match_prog
+               (HTLgenproof.TransfHTLLink HTLgen.transl_program))
   (*::: mkpass (match_if HLSOpts.optim_ram Memorygen.match_prog)*)
   ::: mkpass Veriloggenproof.match_prog
   ::: pass_nil _.
@@ -305,22 +322,36 @@ Theorem transf_hls_match:
 Proof.
   intros p tp T.
   unfold transf_hls, time in T. simpl in T.
-  destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate.
-  destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate.
-  destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate.
-  destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate.
-  destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate.
+  destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1;
+    simpl in T; try discriminate.
+  destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2;
+    simpl in T; try discriminate.
+  destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3;
+    simpl in T; try discriminate.
+  destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4;
+    simpl in T; try discriminate.
+  destruct (Selection.sel_program p4) as [p5|e] eqn:P5;
+    simpl in T; try discriminate.
+  rewrite ! compose_print_identity in T.
+  destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6;
+    simpl in T; try discriminate.
+  unfold transf_backend, time in T. simpl in T.
   rewrite ! compose_print_identity in T.
-  destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate.
-  unfold transf_backend, time in T. simpl in T. rewrite ! compose_print_identity in T.
-  destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate.
+  destruct (Inlining.transf_program p6) as [p7|e] eqn:P7;
+    simpl in T; try discriminate.
   set (p8 := Renumber.transf_program p7) in *.
-  set (p9 := total_if Compopts.optim_constprop Constprop.transf_program p8) in *.
-  set (p10 := total_if Compopts.optim_constprop Renumber.transf_program p9) in *.
-  destruct (partial_if Compopts.optim_CSE CSE.transf_program p10) as [p11|e] eqn:P11; simpl in T; try discriminate.
-  destruct (partial_if Compopts.optim_redundancy Deadcode.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate.
-  destruct (Unusedglob.transform_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate.
-  destruct (HTLgen.transl_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate.
+  set (p9 := total_if Compopts.optim_constprop
+                      Constprop.transf_program p8) in *.
+  set (p10 := total_if Compopts.optim_constprop
+                       Renumber.transf_program p9) in *.
+  destruct (partial_if Compopts.optim_CSE CSE.transf_program p10)
+    as [p11|e] eqn:P11; simpl in T; try discriminate.
+  destruct (partial_if Compopts.optim_redundancy Deadcode.transf_program p11)
+    as [p12|e] eqn:P12; simpl in T; try discriminate.
+  destruct (Unusedglob.transform_program p12) as [p13|e] eqn:P13;
+    simpl in T; try discriminate.
+  destruct (HTLgen.transl_program p13) as [p14|e] eqn:P14;
+    simpl in T; try discriminate.
   (*set (p15 := total_if HLSOpts.optim_ram Memorygen.transf_program p14) in *.*)
   set (p15 := Veriloggen.transl_program p14) in *.
   unfold match_prog; simpl.
@@ -332,13 +363,18 @@ Proof.
   exists p6; split. apply RTLgenproof.transf_program_match; auto.
   exists p7; split. apply Inliningproof.transf_program_match; auto.
   exists p8; split. apply Renumberproof.transf_program_match; auto.
-  exists p9; split. apply total_if_match. apply Constpropproof.transf_program_match.
-  exists p10; split. apply total_if_match. apply Renumberproof.transf_program_match.
-  exists p11; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match.
-  exists p12; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match.
+  exists p9; split. apply total_if_match.
+  apply Constpropproof.transf_program_match.
+  exists p10; split. apply total_if_match.
+  apply Renumberproof.transf_program_match.
+  exists p11; split. eapply partial_if_match; eauto.
+  apply CSEproof.transf_program_match.
+  exists p12; split. eapply partial_if_match; eauto.
+  apply Deadcodeproof.transf_program_match.
   exists p13; split. apply Unusedglobproof.transf_program_match; auto.
   exists p14; split. apply HTLgenproof.transf_program_match; auto.
-  (*exists p15; split. apply total_if_match. apply Memorygen.transf_program_match; auto.*)
+  (*exists p15; split. apply total_if_match.
+    apply Memorygen.transf_program_match; auto.*)
   exists p15; split. apply Veriloggenproof.transf_program_match; auto.
   inv T. reflexivity.
 Qed.
@@ -347,7 +383,8 @@ Theorem cstrategy_semantic_preservation:
   forall p tp,
   match_prog p tp ->
   forward_simulation (Cstrategy.semantics p) (Verilog.semantics tp)
-  /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp).
+  /\ backward_simulation (atomic (Cstrategy.semantics p))
+                         (Verilog.semantics tp).
 Proof.
   intros p tp M. unfold match_prog, pass_match in M; simpl in M.
 Ltac DestructM :=
@@ -357,7 +394,8 @@ Ltac DestructM :=
       destruct H as (p & M & MM); clear H
   end.
   repeat DestructM. subst tp.
-  assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p15)).
+  assert (F: forward_simulation (Cstrategy.semantics p)
+                                (Verilog.semantics p15)).
   {
   eapply compose_forward_simulations.
     eapply SimplExprproof.transl_program_correct; eassumption.
@@ -376,24 +414,30 @@ Ltac DestructM :=
   eapply compose_forward_simulations.
     eapply Renumberproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
-  eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct.
+  eapply match_if_simulation. eassumption.
+  exact Constpropproof.transf_program_correct.
   eapply compose_forward_simulations.
-    eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct.
+    eapply match_if_simulation. eassumption.
+  exact Renumberproof.transf_program_correct.
   eapply compose_forward_simulations.
-    eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct.
+    eapply match_if_simulation. eassumption.
+  exact CSEproof.transf_program_correct.
   eapply compose_forward_simulations.
-    eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption.
+    eapply match_if_simulation. eassumption.
+  exact Deadcodeproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply Unusedglobproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply HTLgenproof.transf_program_correct. eassumption.
   (*eapply compose_forward_simulations.
-    eapply match_if_simulation. eassumption. exact Memorygen.transf_program_correct; eassumption.*)
+    eapply match_if_simulation. eassumption.
+    exact Memorygen.transf_program_correct; eassumption.*)
   eapply Veriloggenproof.transf_program_correct; eassumption.
   }
   split. auto.
   apply forward_to_backward_simulation.
-  apply factor_forward_simulation. auto. eapply sd_traces. eapply Verilog.semantics_determinate.
+  apply factor_forward_simulation. auto. eapply sd_traces.
+  eapply Verilog.semantics_determinate.
   apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive.
   apply Verilog.semantics_determinate.
 Qed.
@@ -451,11 +495,13 @@ Theorem separate_transf_c_program_correct:
   link_list c_units = Some c_program ->
   exists verilog_program,
       link_list verilog_units = Some verilog_program
-   /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program).
+   /\ backward_simulation (Csem.semantics c_program)
+                          (Verilog.semantics verilog_program).
 Proof.
   intros.
   assert (nlist_forall2 match_prog c_units verilog_units).
-  { eapply nlist_forall2_imply. eauto. simpl; intros. apply transf_hls_match; auto. }
+  { eapply nlist_forall2_imply. eauto. simpl; intros.
+    apply transf_hls_match; auto. }
   assert (exists verilog_program, link_list verilog_units = Some verilog_program
                                   /\ match_prog c_program verilog_program).
   { eapply link_list_compose_passes; eauto. }
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index d23850a..d308366 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -1,20 +1,32 @@
-(*
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com>
- *
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as published by
- * the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with this program.  If not, see <https://www.gnu.org/licenses/>.
- *)
+(*|
+..
+   Vericert: Verified high-level synthesis.
+   Copyright (C) 2019-2022 Yann Herklotz <yann@yannherklotz.com>
+
+   This program is free software: you can redistribute it and/or modify
+   it under the terms of the GNU General Public License as published by
+   the Free Software Foundation, either version 3 of the License, or
+   (at your option) any later version.
+
+   This program is distributed in the hope that it will be useful,
+   but WITHOUT ANY WARRANTY; without even the implied warranty of
+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+   GNU General Public License for more details.
+
+   You should have received a copy of the GNU General Public License
+   along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+=============
+RTLBlockInstr
+=============
+
+These instructions are used for ``RTLBlock`` and ``RTLPar``, so that they have
+consistent instructions, which greatly simplifies the proofs, as they will by
+default have the same instruction syntax and semantics.  The only changes are
+therefore at the top-level of the instructions.
+
+.. coq:: none
+|*)
 
 Require Import Coq.micromega.Lia.
 
@@ -34,15 +46,6 @@ Require Import Vericertlib.
 Definition node := positive.
 
 (*|
-=============
-RTLBlockInstr
-=============
-
-These instructions are used for ``RTLBlock`` and ``RTLPar``, so that they have
-consistent instructions, which greatly simplifies the proofs, as they will by
-default have the same instruction syntax and semantics.  The only changes are
-therefore at the top-level of the instructions.
-
 Instruction Definition
 ======================