diff options
Diffstat (limited to 'doc/documentation.org')
| -rw-r--r-- | doc/documentation.org | 562 |
1 files changed, 562 insertions, 0 deletions
diff --git a/doc/documentation.org b/doc/documentation.org new file mode 100644 index 0000000..85bc8fd --- /dev/null +++ b/doc/documentation.org @@ -0,0 +1,562 @@ +#+title: Vericert Manual +#+subtitle: Release {{{version}}} +#+author: Yann Herklotz +#+email: git@ymhg.org +#+language: en + +* Introduction +: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 "600px" +#+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.png]] + +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:../README.org::#building]] :only-contents :exclude-elements "headline property-drawer" +#+transclude: [[file:~/projects/vericert/README.org::#downloading-compcert][file:../README.org::#downloading-compcert]] :level 2 +#+transclude: [[file:~/projects/vericert/README.org::#setting-up-nix][file:../README.org::#setting-up-nix]] :level 2 +#+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: + +#+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 + +** Man pages + +#+transclude: [[file:man.org][file:man.org]] :exclude-elements "keyword" :level 3 + +* 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: +#+cindex: scheduling + +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: res/fdl.org |