Add back pure documentation

5 files changed, 1102 insertions, 0 deletions

diff --git a/docs/README.org b/docs/README.org
new file mode 100644
index 0000000..4113ed9
--- /dev/null
+++ b/docs/README.org
@@ -0,0 +1,7 @@
+#+title: Vericert Documentation
+
+The documentation for [[https://github.com/ymherklotz/vericert][Vericert]], which is written in the [[/documentation.org][documentation.org]] file.
+
+* How to develop on documentation
+
+The documentation uses =hugo= to generate the website,
diff --git a/docs/common.org b/docs/common.org
new file mode 100644
index 0000000..8c39be0
--- /dev/null
+++ b/docs/common.org
@@ -0,0 +1,13 @@
+#+author: Yann Herklotz
+#+email: git@ymhg.org
+
+#+macro: version 1.2.2
+#+macro: modified 2022-02-24
+
+#+macro: link src_emacs-lisp[:results raw]{(ymhg/link "$1" "$2")}
+
+#+macro: texinfo_head (eval (if (eq org-export-current-backend 'texinfo) "#+exclude_tags: noexport_texinfo" "#+exclude_tags: onlyexport_texinfo"))
+#+macro: latex_head (eval (if (eq org-export-current-backend 'latex) "#+exclude_tags: noexport_latex" "#+exclude_tags: onlyexport_latex"))
+#+macro: hugo_head (eval (if (eq org-export-current-backend 'hugo) "#+exclude_tags: noexport_hugo" "#+exclude_tags: onlyexport_hugo"))
+{{{texinfo_head}}}
+{{{latex_head}}}
diff --git a/docs/documentation.org b/docs/documentation.org
new file mode 100644
index 0000000..d4ef799
--- /dev/null
+++ b/docs/documentation.org
@@ -0,0 +1,557 @@
+#+title: Vericert Manual
+#+subtitle: Release {{{version}}}
+#+author:   Yann Herklotz
+#+email:    git@ymhg.org
+#+language: en
+
+* Docs
+:PROPERTIES:
+:EXPORT_FILE_NAME: _index
+:EXPORT_HUGO_SECTION: docs
+:CUSTOM_ID: docs
+:END:
+
+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).
+
+#+attr_html: :width 600
+#+caption: 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.
+#+name: fig:design
+[[/images/toolflow.svg]]
+
+The design shown in Figure [[fig:design]] shows how Vericert leverages an existing verified C compiler
+called [[https://compcert.org/compcert-C.html][CompCert]] to perform this translation.
+
+#+texinfo: @insertcopying
+
+* COPYING
+:PROPERTIES:
+:COPYING: t
+:END:
+
+Copyright (C) 2019-2022  Yann Herklotz.
+
+#+begin_quote
+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''.
+#+end_quote
+
+* Building Vericert
+:PROPERTIES:
+:EXPORT_FILE_NAME: building
+:EXPORT_HUGO_SECTION: docs
+:CUSTOM_ID: building
+:END:
+
+#+transclude: [[file:~/projects/vericert/README.org::#building][file:~/projects/vericert/README.org::#building]] :only-contents :exclude-elements "headline property-drawer"
+#+transclude: [[file:~/projects/vericert/README.org::#downloading-compcert][file:~/projects/vericert/README.org::#downloading-compcert]]
+#+transclude: [[file:~/projects/vericert/README.org::#setting-up-nix][file:~/projects/vericert/README.org::#setting-up-nix]]
+#+transclude: [[file:~/projects/vericert/README.org::#makefile-build][file:~/projects/vericert/README.org::#makefile-build]]
+
+** Testing
+
+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
+
+Or by running the test suite using the following command:
+
+#+begin_src shell
+make test
+#+end_src
+
+* Using Vericert
+:PROPERTIES:
+:CUSTOM_ID: using-vericert
+:END:
+
+Vericert can be used to translate a subset of C into Verilog.  As a simple example, consider the
+following C file (~main.c~):
+
+#+begin_src 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];
+}
+#+end_src
+
+It can be compiled using the following command, assuming that vericert is somewhere on the path.
+
+#+begin_src shell
+vericert main.c -o main.v
+#+end_src
+
+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 [[http://iverilog.icarus.com/][Icarus
+Verilog]] as an example:
+
+#+begin_src shell
+iverilog -o main_v main.v
+#+end_src
+
+When executing, it should therefore print the following:
+
+#+begin_src shell
+$ ./main_v
+finished: 50
+#+end_src
+
+This gives the same result as executing the C in the following way:
+
+#+begin_src shell
+$ gcc -o main_c main.c
+$ ./main_c
+$ echo $?
+50
+#+end_src
+
+* Unreleased Features
+:PROPERTIES:
+:EXPORT_FILE_NAME: unreleased
+:EXPORT_HUGO_SECTION: docs
+:CUSTOM_ID: unreleased-features
+:END:
+
+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][scheduling]],
+- [[#operation-chaining][operation chaining]],
+- [[#if-conversion][if-conversion]], and
+- [[#functions][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
+:PROPERTIES:
+:CUSTOM_ID: scheduling
+:END:
+
+Scheduling is an optimisation which is used to run various instructions in parallel that are
+independent to each other.
+
+** Operation Chaining
+:PROPERTIES:
+:CUSTOM_ID: operation-chaining
+:END:
+
+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
+:PROPERTIES:
+:CUSTOM_ID: if-conversion
+:END:
+
+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
+:PROPERTIES:
+:CUSTOM_ID: functions
+:END:
+
+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
+  :PROPERTIES:
+  :CUSTOM_ID: coq-style-guide
+  :EXPORT_FILE_NAME: coq-style-guide
+  :EXPORT_HUGO_SECTION: docs
+  :END:
+
+This style guide was taken from [[https://github.com/project-oak/silveroak][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.
+
+** Code organization
+   :PROPERTIES:
+   :CUSTOM_ID: code-organization
+   :END:
+*** Legal banner
+    :PROPERTIES:
+    :CUSTOM_ID: legal-banner
+    :END:
+
+- Files should begin with a copyright/license banner, as shown in the example above.
+
+*** Import statements
+    :PROPERTIES:
+    :CUSTOM_ID: import-statements
+    :END:
+
+- =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
+    :PROPERTIES:
+    :CUSTOM_ID: notations-and-scopes
+    :END:
+
+- 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
+   :PROPERTIES:
+   :CUSTOM_ID: formatting
+   :END:
+*** Line length
+    :PROPERTIES:
+    :CUSTOM_ID: line-length
+    :END:
+
+- 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
+    :PROPERTIES:
+    :CUSTOM_ID: whitespace-and-indentation
+    :END:
+
+- 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:
+
+  #+begin_src coq
+    (Z.pow
+       1 2)
+    (Z.pow 1 2 3
+           4 5 6)
+  #+end_src
+
+- =Inductive= cases should not be indented. Example:
+
+  #+begin_src coq
+    Inductive Foo : Type :=
+    | FooA : Foo
+    | FooB : Foo
+    .
+  #+end_src
+
+- =match= or =lazymatch= cases should line up with the "m" in =match= or "l" in =lazymatch=, as in the
+  following examples:
+
+  #+begin_src 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.
+  #+end_src
+
+** Definitions and Fixpoints
+   :PROPERTIES:
+   :CUSTOM_ID: definitions-and-fixpoints
+   :END:
+
+- 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
+   :PROPERTIES:
+   :CUSTOM_ID: inductives
+   :END:
+
+- 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:
+
+  #+begin_src coq
+    Inductive Foo : Type :=
+    | FooA : Foo
+    | FooB : Foo
+    .
+    Inductive Foo : Type :=
+    | FooA : Foo
+    | FooB : Foo.
+  #+end_src
+
+** Lemma/Theorem statements
+   :PROPERTIES:
+   :CUSTOM_ID: lemmatheorem-statements
+   :END:
+
+- 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
+   :PROPERTIES:
+   :CUSTOM_ID: proofs-and-tactics
+   :END:
+
+- 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:
+
+  #+begin_src coq
+    Ltac crush_step :=
+      match goal with
+      | _ => progress subst
+      | _ => reflexivity
+      end.
+    Ltac crush := repeat crush_step.
+  #+end_src
+
+** Naming
+   :PROPERTIES:
+   :CUSTOM_ID: naming
+   :END:
+
+- 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
+   :PROPERTIES:
+   :CUSTOM_ID: example
+   :END:
+A small standalone Coq file that exhibits many of the style points.
+
+#+begin_src 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.
+#+end_src
+
+* Index - Features
+:PROPERTIES:
+:CUSTOM_ID: cindex
+:APPENDIX: t
+:INDEX:    cp
+:DESCRIPTION: Key concepts & features
+:END:
+
+* Export Setup :noexport:
+
+#+setupfile: common.org
+
+#+export_file_name: vericert.texi
+
+#+texinfo_dir_category: High-level synthesis tool
+#+texinfo_dir_title: Vericert
+#+texinfo_dir_desc: Formally verified high-level synthesis tool
+
+* GNU Free Documentation License
+:PROPERTIES:
+:appendix: t
+:END:
+
+#+include: fdl.org
diff --git a/docs/fdl.org b/docs/fdl.org
new file mode 100644
index 0000000..81e2cd9
--- /dev/null
+++ b/docs/fdl.org
@@ -0,0 +1,489 @@
+# The GNU Free Documentation License.
+#+begin_center
+Version 1.3, 3 November 2008
+#+end_center
+
+# This file is intended to be included within another document.
+
+#+begin_verse
+Copyright \copy{} 2000, 2001, 2002, 2007, 2008 Free Software Foundation, Inc.
+https://fsf.org/
+
+Everyone is permitted to copy and distribute verbatim copies
+of this license document, but changing it is not allowed.
+#+end_verse
+
+0. [@0] PREAMBLE
+
+   The purpose of this License is to make a manual, textbook, or other
+   functional and useful document @@texinfo:@dfn{@@free@@texinfo:}@@
+   in the sense of freedom: to assure everyone the effective freedom
+   to copy and redistribute it, with or without modifying it, either
+   commercially or noncommercially. Secondarily, this License
+   preserves for the author and publisher a way to get credit for
+   their work, while not being considered responsible for
+   modifications made by others.
+
+   This License is a kind of "copyleft", which means that derivative
+   works of the document must themselves be free in the same sense.
+   It complements the GNU General Public License, which is a copyleft
+   license designed for free software.
+
+   We have designed this License in order to use it for manuals for
+   free software, because free software needs free documentation:
+   a free program should come with manuals providing the same freedoms
+   that the software does.  But this License is not limited to
+   software manuals; it can be used for any textual work, regardless
+   of subject matter or whether it is published as a printed book.  We
+   recommend this License principally for works whose purpose is
+   instruction or reference.
+
+1. APPLICABILITY AND DEFINITIONS
+
+   This License applies to any manual or other work, in any medium,
+   that contains a notice placed by the copyright holder saying it can
+   be distributed under the terms of this License.  Such a notice
+   grants a world-wide, royalty-free license, unlimited in duration,
+   to use that work under the conditions stated herein.  The
+   "Document", below, refers to any such manual or work.  Any member
+   of the public is a licensee, and is addressed as "you".  You accept
+   the license if you copy, modify or distribute the work in a way
+   requiring permission under copyright law.
+
+   A "Modified Version" of the Document means any work containing the
+   Document or a portion of it, either copied verbatim, or with
+   modifications and/or translated into another language.
+
+   A "Secondary Section" is a named appendix or a front-matter section
+   of the Document that deals exclusively with the relationship of the
+   publishers or authors of the Document to the Document's overall
+   subject (or to related matters) and contains nothing that could
+   fall directly within that overall subject.  (Thus, if the Document
+   is in part a textbook of mathematics, a Secondary Section may not
+   explain any mathematics.)  The relationship could be a matter of
+   historical connection with the subject or with related matters, or
+   of legal, commercial, philosophical, ethical or political position
+   regarding them.
+
+   The "Invariant Sections" are certain Secondary Sections whose
+   titles are designated, as being those of Invariant Sections, in the
+   notice that says that the Document is released under this License.
+   If a section does not fit the above definition of Secondary then it
+   is not allowed to be designated as Invariant.  The Document may
+   contain zero Invariant Sections.  If the Document does not identify
+   any Invariant Sections then there are none.
+
+   The "Cover Texts" are certain short passages of text that are
+   listed, as Front-Cover Texts or Back-Cover Texts, in the notice
+   that says that the Document is released under this License.
+   A Front-Cover Text may be at most 5 words, and a Back-Cover Text
+   may be at most 25 words.
+
+   A "Transparent" copy of the Document means a machine-readable copy,
+   represented in a format whose specification is available to the
+   general public, that is suitable for revising the document
+   straightforwardly with generic text editors or (for images composed
+   of pixels) generic paint programs or (for drawings) some widely
+   available drawing editor, and that is suitable for input to text
+   formatters or for automatic translation to a variety of formats
+   suitable for input to text formatters.  A copy made in an otherwise
+   Transparent file format whose markup, or absence of markup, has
+   been arranged to thwart or discourage subsequent modification by
+   readers is not Transparent.  An image format is not Transparent if
+   used for any substantial amount of text.  A copy that is not
+   "Transparent" is called "Opaque".
+
+   Examples of suitable formats for Transparent copies include plain
+   ASCII without markup, Texinfo input format, LaTeX input format,
+   SGML or XML using a publicly available DTD, and standard-conforming
+   simple HTML, PostScript or PDF designed for human modification.
+   Examples of transparent image formats include PNG, XCF and JPG.
+   Opaque formats include proprietary formats that can be read and
+   edited only by proprietary word processors, SGML or XML for which
+   the DTD and/or processing tools are not generally available, and
+   the machine-generated HTML, PostScript or PDF produced by some word
+   processors for output purposes only.
+
+   The "Title Page" means, for a printed book, the title page itself,
+   plus such following pages as are needed to hold, legibly, the
+   material this License requires to appear in the title page.  For
+   works in formats which do not have any title page as such, "Title
+   Page" means the text near the most prominent appearance of the
+   work's title, preceding the beginning of the body of the text.
+
+   The "publisher" means any person or entity that distributes copies
+   of the Document to the public.
+
+   A section "Entitled XYZ" means a named subunit of the Document
+   whose title either is precisely XYZ or contains XYZ in parentheses
+   following text that translates XYZ in another language.  (Here XYZ
+   stands for a specific section name mentioned below, such as
+   "Acknowledgements", "Dedications", "Endorsements", or "History".)
+   To "Preserve the Title" of such a section when you modify the
+   Document means that it remains a section "Entitled XYZ" according
+   to this definition.
+
+   The Document may include Warranty Disclaimers next to the notice
+   which states that this License applies to the Document.  These
+   Warranty Disclaimers are considered to be included by reference in
+   this License, but only as regards disclaiming warranties: any other
+   implication that these Warranty Disclaimers may have is void and
+   has no effect on the meaning of this License.
+
+2. VERBATIM COPYING
+
+   You may copy and distribute the Document in any medium, either
+   commercially or noncommercially, provided that this License, the
+   copyright notices, and the license notice saying this License
+   applies to the Document are reproduced in all copies, and that you
+   add no other conditions whatsoever to those of this License.  You
+   may not use technical measures to obstruct or control the reading
+   or further copying of the copies you make or distribute.  However,
+   you may accept compensation in exchange for copies.  If you
+   distribute a large enough number of copies you must also follow the
+   conditions in section 3.
+
+   You may also lend copies, under the same conditions stated above,
+   and you may publicly display copies.
+
+3. COPYING IN QUANTITY
+
+   If you publish printed copies (or copies in media that commonly
+   have printed covers) of the Document, numbering more than 100, and
+   the Document's license notice requires Cover Texts, you must
+   enclose the copies in covers that carry, clearly and legibly, all
+   these Cover Texts: Front-Cover Texts on the front cover, and
+   Back-Cover Texts on the back cover.  Both covers must also clearly
+   and legibly identify you as the publisher of these copies.  The
+   front cover must present the full title with all words of the title
+   equally prominent and visible.  You may add other material on the
+   covers in addition.  Copying with changes limited to the covers, as
+   long as they preserve the title of the Document and satisfy these
+   conditions, can be treated as verbatim copying in other respects.
+
+   If the required texts for either cover are too voluminous to fit
+   legibly, you should put the first ones listed (as many as fit
+   reasonably) on the actual cover, and continue the rest onto
+   adjacent pages.
+
+   If you publish or distribute Opaque copies of the Document
+   numbering more than 100, you must either include a machine-readable
+   Transparent copy along with each Opaque copy, or state in or with
+   each Opaque copy a computer-network location from which the general
+   network-using public has access to download using public-standard
+   network protocols a complete Transparent copy of the Document, free
+   of added material.  If you use the latter option, you must take
+   reasonably prudent steps, when you begin distribution of Opaque
+   copies in quantity, to ensure that this Transparent copy will
+   remain thus accessible at the stated location until at least one
+   year after the last time you distribute an Opaque copy (directly or
+   through your agents or retailers) of that edition to the public.
+
+   It is requested, but not required, that you contact the authors of
+   the Document well before redistributing any large number of copies,
+   to give them a chance to provide you with an updated version of the
+   Document.
+
+4. MODIFICATIONS
+
+   You may copy and distribute a Modified Version of the Document
+   under the conditions of sections 2 and 3 above, provided that you
+   release the Modified Version under precisely this License, with the
+   Modified Version filling the role of the Document, thus licensing
+   distribution and modification of the Modified Version to whoever
+   possesses a copy of it.  In addition, you must do these things in
+   the Modified Version:
+
+   #+attr_texinfo: :enum A
+   1. Use in the Title Page (and on the covers, if any) a title
+      distinct from that of the Document, and from those of previous
+      versions (which should, if there were any, be listed in the
+      History section of the Document). You may use the same title as
+      a previous version if the original publisher of that version
+      gives permission.
+
+   2. List on the Title Page, as authors, one or more persons or
+      entities responsible for authorship of the modifications in the
+      Modified Version, together with at least five of the principal
+      authors of the Document (all of its principal authors, if it has
+      fewer than five), unless they release you from this requirement.
+
+   3. State on the Title page the name of the publisher of the
+      Modified Version, as the publisher.
+
+   4. Preserve all the copyright notices of the Document.
+
+   5. Add an appropriate copyright notice for your modifications
+      adjacent to the other copyright notices.
+
+   6. Include, immediately after the copyright notices, a license
+      notice giving the public permission to use the Modified Version
+      under the terms of this License, in the form shown in the
+      Addendum below.
+
+   7. Preserve in that license notice the full lists of Invariant
+      Sections and required Cover Texts given in the Document's
+      license notice.
+
+   8. Include an unaltered copy of this License.
+
+   9. Preserve the section Entitled "History", Preserve its Title, and
+      add to it an item stating at least the title, year, new authors,
+      and publisher of the Modified Version as given on the Title
+      Page. If there is no section Entitled "History" in the Document,
+      create one stating the title, year, authors, and publisher of
+      the Document as given on its Title Page, then add an item
+      describing the Modified Version as stated in the previous
+      sentence.
+
+   10. Preserve the network location, if any, given in the Document
+       for public access to a Transparent copy of the Document, and
+       likewise the network locations given in the Document for
+       previous versions it was based on. These may be placed in the
+       "History" section. You may omit a network location for a work
+       that was published at least four years before the Document
+       itself, or if the original publisher of the version it refers
+       to gives permission.
+
+   11. For any section Entitled "Acknowledgements" or "Dedications",
+       Preserve the Title of the section, and preserve in the section
+       all the substance and tone of each of the contributor
+       acknowledgements and/or dedications given therein.
+
+   12. Preserve all the Invariant Sections of the Document, unaltered
+       in their text and in their titles. Section numbers or the
+       equivalent are not considered part of the section titles.
+
+   13. Delete any section Entitled "Endorsements". Such a section may
+       not be included in the Modified Version.
+
+   14. Do not retitle any existing section to be Entitled
+       "Endorsements" or to conflict in title with any Invariant
+       Section.
+
+   15. Preserve any Warranty Disclaimers.
+
+   If the Modified Version includes new front-matter sections or
+   appendices that qualify as Secondary Sections and contain no material
+   copied from the Document, you may at your option designate some or all
+   of these sections as invariant.  To do this, add their titles to the
+   list of Invariant Sections in the Modified Version's license notice.
+   These titles must be distinct from any other section titles.
+
+   You may add a section Entitled "Endorsements", provided it contains
+   nothing but endorsements of your Modified Version by various
+   parties---for example, statements of peer review or that the text has
+   been approved by an organization as the authoritative definition of a
+   standard.
+
+   You may add a passage of up to five words as a Front-Cover Text, and a
+   passage of up to 25 words as a Back-Cover Text, to the end of the list
+   of Cover Texts in the Modified Version.  Only one passage of
+   Front-Cover Text and one of Back-Cover Text may be added by (or
+   through arrangements made by) any one entity.  If the Document already
+   includes a cover text for the same cover, previously added by you or
+   by arrangement made by the same entity you are acting on behalf of,
+   you may not add another; but you may replace the old one, on explicit
+   permission from the previous publisher that added the old one.
+
+   The author(s) and publisher(s) of the Document do not by this License
+   give permission to use their names for publicity for or to assert or
+   imply endorsement of any Modified Version.
+
+5. COMBINING DOCUMENTS
+
+   You may combine the Document with other documents released under
+   this License, under the terms defined in section 4 above for
+   modified versions, provided that you include in the combination all
+   of the Invariant Sections of all of the original documents,
+   unmodified, and list them all as Invariant Sections of your
+   combined work in its license notice, and that you preserve all
+   their Warranty Disclaimers.
+
+   The combined work need only contain one copy of this License, and
+   multiple identical Invariant Sections may be replaced with a single
+   copy.  If there are multiple Invariant Sections with the same name
+   but different contents, make the title of each such section unique
+   by adding at the end of it, in parentheses, the name of the
+   original author or publisher of that section if known, or else
+   a unique number.  Make the same adjustment to the section titles in
+   the list of Invariant Sections in the license notice of the
+   combined work.
+
+   In the combination, you must combine any sections Entitled
+   "History" in the various original documents, forming one section
+   Entitled "History"; likewise combine any sections Entitled
+   "Acknowledgements", and any sections Entitled "Dedications".  You
+   must delete all sections Entitled "Endorsements."
+
+6. COLLECTIONS OF DOCUMENTS
+
+   You may make a collection consisting of the Document and other
+   documents released under this License, and replace the individual
+   copies of this License in the various documents with a single copy
+   that is included in the collection, provided that you follow the
+   rules of this License for verbatim copying of each of the documents
+   in all other respects.
+
+   You may extract a single document from such a collection, and
+   distribute it individually under this License, provided you insert
+   a copy of this License into the extracted document, and follow this
+   License in all other respects regarding verbatim copying of that
+   document.
+
+7. AGGREGATION WITH INDEPENDENT WORKS
+
+   A compilation of the Document or its derivatives with other
+   separate and independent documents or works, in or on a volume of
+   a storage or distribution medium, is called an "aggregate" if the
+   copyright resulting from the compilation is not used to limit the
+   legal rights of the compilation's users beyond what the individual
+   works permit.  When the Document is included in an aggregate, this
+   License does not apply to the other works in the aggregate which
+   are not themselves derivative works of the Document.
+
+   If the Cover Text requirement of section 3 is applicable to these
+   copies of the Document, then if the Document is less than one half
+   of the entire aggregate, the Document's Cover Texts may be placed
+   on covers that bracket the Document within the aggregate, or the
+   electronic equivalent of covers if the Document is in electronic
+   form.  Otherwise they must appear on printed covers that bracket
+   the whole aggregate.
+
+8. TRANSLATION
+
+   Translation is considered a kind of modification, so you may
+   distribute translations of the Document under the terms of
+   section 4.  Replacing Invariant Sections with translations requires
+   special permission from their copyright holders, but you may
+   include translations of some or all Invariant Sections in addition
+   to the original versions of these Invariant Sections.  You may
+   include a translation of this License, and all the license notices
+   in the Document, and any Warranty Disclaimers, provided that you
+   also include the original English version of this License and the
+   original versions of those notices and disclaimers.  In case of
+   a disagreement between the translation and the original version of
+   this License or a notice or disclaimer, the original version will
+   prevail.
+
+   If a section in the Document is Entitled "Acknowledgements",
+   "Dedications", or "History", the requirement (section 4) to
+   Preserve its Title (section 1) will typically require changing the
+   actual title.
+
+9. TERMINATION
+
+   You may not copy, modify, sublicense, or distribute the Document
+   except as expressly provided under this License.  Any attempt
+   otherwise to copy, modify, sublicense, or distribute it is void,
+   and will automatically terminate your rights under this License.
+
+   However, if you cease all violation of this License, then your
+   license from a particular copyright holder is reinstated (a)
+   provisionally, unless and until the copyright holder explicitly and
+   finally terminates your license, and (b) permanently, if the
+   copyright holder fails to notify you of the violation by some
+   reasonable means prior to 60 days after the cessation.
+
+   Moreover, your license from a particular copyright holder is
+   reinstated permanently if the copyright holder notifies you of the
+   violation by some reasonable means, this is the first time you have
+   received notice of violation of this License (for any work) from
+   that copyright holder, and you cure the violation prior to 30 days
+   after your receipt of the notice.
+
+   Termination of your rights under this section does not terminate
+   the licenses of parties who have received copies or rights from you
+   under this License.  If your rights have been terminated and not
+   permanently reinstated, receipt of a copy of some or all of the
+   same material does not give you any rights to use it.
+
+10. FUTURE REVISIONS OF THIS LICENSE
+
+    The Free Software Foundation may publish new, revised versions of
+    the GNU Free Documentation License from time to time.  Such new
+    versions will be similar in spirit to the present version, but may
+    differ in detail to address new problems or concerns.  See
+    https://www.gnu.org/copyleft/.
+
+    Each version of the License is given a distinguishing version
+    number.  If the Document specifies that a particular numbered
+    version of this License "or any later version" applies to it, you
+    have the option of following the terms and conditions either of
+    that specified version or of any later version that has been
+    published (not as a draft) by the Free Software Foundation.  If
+    the Document does not specify a version number of this License,
+    you may choose any version ever published (not as a draft) by the
+    Free Software Foundation.  If the Document specifies that a proxy
+    can decide which future versions of this License can be used, that
+    proxy's public statement of acceptance of a version permanently
+    authorizes you to choose that version for the Document.
+
+11. RELICENSING
+
+    "Massive Multiauthor Collaboration Site" (or "MMC Site") means any
+    World Wide Web server that publishes copyrightable works and also
+    provides prominent facilities for anybody to edit those works.
+    A public wiki that anybody can edit is an example of such
+    a server.  A "Massive Multiauthor Collaboration" (or "MMC")
+    contained in the site means any set of copyrightable works thus
+    published on the MMC site.
+
+    "CC-BY-SA" means the Creative Commons Attribution-Share Alike 3.0
+    license published by Creative Commons Corporation,
+    a not-for-profit corporation with a principal place of business in
+    San Francisco, California, as well as future copyleft versions of
+    that license published by that same organization.
+
+    "Incorporate" means to publish or republish a Document, in whole
+    or in part, as part of another Document.
+
+    An MMC is "eligible for relicensing" if it is licensed under this
+    License, and if all works that were first published under this
+    License somewhere other than this MMC, and subsequently
+    incorporated in whole or in part into the MMC, (1) had no cover
+    texts or invariant sections, and (2) were thus incorporated prior
+    to November 1, 2008.
+
+    The operator of an MMC Site may republish an MMC contained in the
+    site under CC-BY-SA on the same site at any time before August 1,
+    2009, provided the MMC is eligible for relicensing.
+
+#+texinfo: @page
+
+* ADDENDUM: How to use this License for your documents
+:PROPERTIES:
+:UNNUMBERED: notoc
+:END:
+
+To use this License in a document you have written, include a copy of
+the License in the document and put the following copyright and
+license notices just after the title page:
+
+#+begin_example
+    Copyright (C)  YEAR  YOUR NAME.
+    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''.
+#+end_example
+
+If you have Invariant Sections, Front-Cover Texts and Back-Cover Texts,
+replace the "with...Texts."\nbsp{}line with this:
+
+#+begin_example
+      with the Invariant Sections being LIST THEIR TITLES, with
+      the Front-Cover Texts being LIST, and with the Back-Cover Texts
+      being LIST.
+#+end_example
+
+If you have Invariant Sections without Cover Texts, or some other
+combination of the three, merge those two alternatives to suit the
+situation.
+
+If your document contains nontrivial examples of program code, we
+recommend releasing these examples in parallel under your choice of
+free software license, such as the GNU General Public License, to
+permit their use in free software.
diff --git a/docs/man.org b/docs/man.org
new file mode 100644
index 0000000..279165c
--- /dev/null
+++ b/docs/man.org
@@ -0,0 +1,36 @@
+#+title: vericert
+#+man_class_options: :section-id "1"
+#+export_file_name: vericert.1
+
+* NAME
+
+vericert - A formally verified high-level synthesis tool.
+
+* SYNOPSYS
+
+*vericert* [ *OPTION* ]... [ *FILE* ]...
+
+* DESCRIPTION
+
+- -drtl :: Print intermediate RTL.
+
+* AUTHOR
+
+Written by Yann Herklotz, Michalis Pardalos, James Pollard, Nadesh Ramanathan and John Wickerson.
+
+* COPYRIGHT
+
+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/>.