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