From 11d6215f265d0dbcfd0048819a614f318a0775a4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 26 Mar 2022 21:08:23 +0000 Subject: Add sphinx documentation --- .gitignore | 4 +- Makefile | 3 +- doc/Makefile | 24 + doc/Makefile.extr | 39 ++ doc/README.org | 7 + doc/_static/css/custom.css | 11 + doc/_static/images/toolflow.pdf | Bin 0 -> 20490 bytes doc/_static/images/toolflow.png | Bin 0 -> 26864 bytes doc/_static/images/toolflow.svg | 1250 +++++++++++++++++++++++++++++++++++++++ doc/common.org | 15 + doc/conf.py | 85 +++ doc/documentation.org | 562 ++++++++++++++++++ doc/docutils.conf | 2 + doc/index.rst | 26 + doc/make.bat | 35 ++ doc/man.org | 89 +++ doc/res/coqdoc.css | 867 +++++++++++++++++++++++++++ doc/res/fdl.org | 489 +++++++++++++++ doc/res/install-deps.el | 11 + doc/res/publish.el | 23 + doc/vericert.rst | 530 +++++++++++++++++ docs/Makefile | 39 -- docs/README.org | 7 - docs/common.org | 15 - docs/documentation.org | 562 ------------------ docs/images/toolflow.pdf | Bin 20490 -> 0 bytes docs/images/toolflow.png | Bin 26864 -> 0 bytes docs/images/toolflow.svg | 1250 --------------------------------------- docs/man.org | 89 --- docs/res/coqdoc.css | 867 --------------------------- docs/res/fdl.org | 489 --------------- docs/res/install-deps.el | 11 - docs/res/publish.el | 23 - src/Compiler.v | 172 ++++-- src/hls/RTLBlockInstr.v | 55 +- 35 files changed, 4206 insertions(+), 3445 deletions(-) create mode 100644 doc/Makefile create mode 100644 doc/Makefile.extr create mode 100644 doc/README.org create mode 100644 doc/_static/css/custom.css create mode 100644 doc/_static/images/toolflow.pdf create mode 100644 doc/_static/images/toolflow.png create mode 100644 doc/_static/images/toolflow.svg create mode 100644 doc/common.org create mode 100644 doc/conf.py create mode 100644 doc/documentation.org create mode 100644 doc/docutils.conf create mode 100644 doc/index.rst create mode 100644 doc/make.bat create mode 100644 doc/man.org create mode 100644 doc/res/coqdoc.css create mode 100644 doc/res/fdl.org create mode 100644 doc/res/install-deps.el create mode 100644 doc/res/publish.el create mode 100644 doc/vericert.rst delete mode 100644 docs/Makefile delete mode 100644 docs/README.org delete mode 100644 docs/common.org delete mode 100644 docs/documentation.org delete mode 100644 docs/images/toolflow.pdf delete mode 100644 docs/images/toolflow.png delete mode 100644 docs/images/toolflow.svg delete mode 100644 docs/man.org delete mode 100644 docs/res/coqdoc.css delete mode 100644 docs/res/fdl.org delete mode 100644 docs/res/install-deps.el delete mode 100644 docs/res/publish.el diff --git a/.gitignore b/.gitignore index 6568d8d..5574171 100644 --- a/.gitignore +++ b/.gitignore @@ -83,9 +83,7 @@ obj_dir/ creduce_bug_*/ -/docs/man/ -/docs/manual/ -/docs/src/ +/doc/src/ /html/ *~ diff --git a/Makefile b/Makefile index a6aa914..3128c23 100644 --- a/Makefile +++ b/Makefile @@ -17,7 +17,8 @@ COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source COQMAKE := $(COQBIN)coq_makefile COQDOCFLAGS := --no-lib-name -l -ALECTRYON_OPTS := --html-minification --long-line-threshold 80 --coq-driver sertop_noexec $(COQINCLUDES) +ALECTRYON_OPTS := --no-header --html-minification --long-line-threshold 80 \ + --coq-driver sertop_noexec $(COQINCLUDES) VS := src/Compiler.v src/Simulator.v src/HLSOpts.v $(foreach d, common hls bourdoncle, $(wildcard src/$(d)/*.v)) LIT := docs/basic-block-generation.org docs/scheduler.org docs/scheduler-languages.org diff --git a/doc/Makefile b/doc/Makefile new file mode 100644 index 0000000..5662645 --- /dev/null +++ b/doc/Makefile @@ -0,0 +1,24 @@ +# Minimal makefile for Sphinx documentation +# + +# You can set these variables from the command line, and also +# from the environment for the first two. +SPHINXOPTS ?= +SPHINXBUILD ?= sphinx-build +SOURCEDIR = . +BUILDDIR = _build +SOURCE_DATE_EPOCH = $(shell git log -1 --format=%ct) + +VS_DOCS := ../src/Compiler.v ../src/hls/RTLBlockInstr.v + +# Put it first so that "make" without argument is like "make help". +help: + @$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) + +.PHONY: help Makefile + +# Catch-all target: route all unknown targets to Sphinx using the new +# "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS). +%: Makefile + $(foreach d,$(VS_DOCS),cp $(d) $(patsubst ../%,%,$(d));) + @$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) diff --git a/doc/Makefile.extr b/doc/Makefile.extr new file mode 100644 index 0000000..9d4f361 --- /dev/null +++ b/doc/Makefile.extr @@ -0,0 +1,39 @@ +all: manual src man-html + +install-deps: + emacs --batch --load ./res/install-deps.el + +%.man: %.org + emacs --batch --file $< --load ./res/publish.el --funcall org-man-export-to-man + +%.html: %.org + emacs --batch --file $< --load ./res/publish.el --funcall org-html-export-to-html + +manual: + mkdir -p manual + emacs --batch --file documentation.org --load ./res/publish.el --funcall org-texinfo-export-to-texinfo + 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/. + +man-html: man.html + mkdir -p man + cp man.html ./man/vericert.1.html + +vericert.1: man.man + cp $< $@ + +src: + $(MAKE) -C .. doc + cp -r ../html src + +upload: + tar caf docs.tar.xz manual man src + rsync docs.tar.xz "zk@leika.ymhg.org:~" + +.PHONY: all upload manual man src install-deps man-html + +clean: + rm -rf manual man src + rm -f docs.tar.xz diff --git a/doc/README.org b/doc/README.org new file mode 100644 index 0000000..4113ed9 --- /dev/null +++ b/doc/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/doc/_static/css/custom.css b/doc/_static/css/custom.css new file mode 100644 index 0000000..66a1e35 --- /dev/null +++ b/doc/_static/css/custom.css @@ -0,0 +1,11 @@ +.alectryon-coqdoc .doc .code, +.alectryon-coqdoc .doc .comment, +.alectryon-coqdoc .doc .inlinecode, +.alectryon-mref, +.alectryon-block, .alectryon-io, +.alectryon-toggle-label, .alectryon-banner, pre, tt, code { + font-family: 'Iosevka Fixed Slab', 'Iosevka Slab Web', 'Iosevka Web', 'Iosevka Slab', + 'Iosevka', 'Fira Code', monospace; + font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */; + line-height: initial; +} diff --git a/doc/_static/images/toolflow.pdf b/doc/_static/images/toolflow.pdf new file mode 100644 index 0000000..5fcee67 Binary files /dev/null and b/doc/_static/images/toolflow.pdf differ diff --git a/doc/_static/images/toolflow.png b/doc/_static/images/toolflow.png new file mode 100644 index 0000000..601d6be Binary files /dev/null and b/doc/_static/images/toolflow.png differ diff --git a/doc/_static/images/toolflow.svg b/doc/_static/images/toolflow.svg new file mode 100644 index 0000000..0d8f39f --- /dev/null +++ b/doc/_static/images/toolflow.svg @@ -0,0 +1,1250 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/doc/common.org b/doc/common.org new file mode 100644 index 0000000..aa27264 --- /dev/null +++ b/doc/common.org @@ -0,0 +1,15 @@ +#+author: Yann Herklotz +#+email: git@ymhg.org + +#+macro: version 1.2.2 +#+macro: modified 2022-02-24 + +#+macro: base_url https://vericert.ymhg.org + +#+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/doc/conf.py b/doc/conf.py new file mode 100644 index 0000000..015f030 --- /dev/null +++ b/doc/conf.py @@ -0,0 +1,85 @@ +# Configuration file for the Sphinx documentation builder. +# +# This file only contains a selection of the most common options. For a full +# list see the documentation: +# https://www.sphinx-doc.org/en/master/usage/configuration.html + +# -- Path setup -------------------------------------------------------------- + +# If extensions (or modules to document with autodoc) are in another directory, +# add these directories to sys.path here. If the directory is relative to the +# documentation root, use os.path.abspath to make it absolute, like shown here. +# +# import os +# import sys +# sys.path.insert(0, os.path.abspath('.')) + + +# -- Project information ----------------------------------------------------- + +project = 'Vericert' +copyright = '2022 Yann Herklotz, John Wickerson' +author = 'Yann Herklotz, John Wickerson' + +# The full version, including alpha/beta/rc tags +release = 'v1.2.2' + + +# -- General configuration --------------------------------------------------- + +# Add any Sphinx extension module names here, as strings. They can be +# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom +# ones. +extensions = [ "alectryon.sphinx" ] + +# Add any paths that contain templates here, relative to this directory. +templates_path = ['_templates'] + +# List of patterns, relative to source directory, that match files and +# directories to ignore when looking for source files. +# This pattern also affects html_static_path and html_extra_path. +exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store'] + +pygments_style = "emacs" + + +# -- Options for HTML output ------------------------------------------------- + +# The theme to use for HTML and HTML Help pages. See the documentation for +# a list of builtin themes. +# +html_theme = 'alabaster' + +# Add any paths that contain custom static files (such as style sheets) here, +# relative to this directory. They are copied after the builtin static files, +# so a file named "default.css" will overwrite the builtin "default.css". +html_static_path = ['_static'] + +html_css_files = [ + 'css/custom.css', +] + + +# -- LaTeX configuration ----------------------------------------------------- + +latex_engine = "xelatex" + + +# -- Alectryon configuration ------------------------------------------------- + +import alectryon.docutils +alectryon.docutils.CACHE_DIRECTORY = "_build/alectryon/" +alectryon.docutils.LONG_LINE_THRESHOLD = 80 + +alectryon.docutils.AlectryonTransform.DRIVER_ARGS["sertop"] = [ + "-R" "../src,vericert", + "-R" "../lib/CompCert/lib,compcert.lib", + "-R" "../lib/CompCert/common,compcert.common", + "-R" "../lib/CompCert/verilog,compcert.verilog", + "-R" "../lib/CompCert/backend,compcert.backend", + "-R" "../lib/CompCert/cfrontend,compcert.cfrontend", + "-R" "../lib/CompCert/driver,compcert.driver", + "-R" "../lib/CompCert/cparser,compcert.cparser", + "-R" "../lib/CompCert/flocq,Flocq", + "-R" "../lib/CompCert/MenhirLib,MenhirLib" +] diff --git a/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. 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 =_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 + * + * + *) + + 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 diff --git a/doc/docutils.conf b/doc/docutils.conf new file mode 100644 index 0000000..1bf4d83 --- /dev/null +++ b/doc/docutils.conf @@ -0,0 +1,2 @@ +[restructuredtext parser] +syntax_highlight = short diff --git a/doc/index.rst b/doc/index.rst new file mode 100644 index 0000000..ebb99df --- /dev/null +++ b/doc/index.rst @@ -0,0 +1,26 @@ +.. Vericert documentation master file, created by + sphinx-quickstart on Sat Mar 26 18:15:40 2022. + You can adapt this file completely to your liking, but it should at least + contain the root `toctree` directive. + +Vericert's Documentation +======================== + +.. toctree:: + :maxdepth: 2 + :caption: Content: + + vericert + +.. toctree:: + :maxdepth: 1 + :caption: Sources: + + src/Compiler + src/hls/RTLBlockInstr + +Indices +================== + +* :ref:`genindex` +* :ref:`search` diff --git a/doc/make.bat b/doc/make.bat new file mode 100644 index 0000000..153be5e --- /dev/null +++ b/doc/make.bat @@ -0,0 +1,35 @@ +@ECHO OFF + +pushd %~dp0 + +REM Command file for Sphinx documentation + +if "%SPHINXBUILD%" == "" ( + set SPHINXBUILD=sphinx-build +) +set SOURCEDIR=. +set BUILDDIR=_build + +if "%1" == "" goto help + +%SPHINXBUILD% >NUL 2>NUL +if errorlevel 9009 ( + echo. + echo.The 'sphinx-build' command was not found. Make sure you have Sphinx + echo.installed, then set the SPHINXBUILD environment variable to point + echo.to the full path of the 'sphinx-build' executable. Alternatively you + echo.may add the Sphinx directory to PATH. + echo. + echo.If you don't have Sphinx installed, grab it from + echo.https://www.sphinx-doc.org/ + exit /b 1 +) + +%SPHINXBUILD% -M %1 %SOURCEDIR% %BUILDDIR% %SPHINXOPTS% %O% +goto end + +:help +%SPHINXBUILD% -M help %SOURCEDIR% %BUILDDIR% %SPHINXOPTS% %O% + +:end +popd diff --git a/doc/man.org b/doc/man.org new file mode 100644 index 0000000..cb6143f --- /dev/null +++ b/doc/man.org @@ -0,0 +1,89 @@ +#+title: vericert +#+man_class_options: :section-id "1" +#+options: toc:nil num:nil +#+html_head_extra: + +* NAME + +vericert - A formally verified high-level synthesis tool. + +* SYNOPSYS + +*vericert* [ *OPTION* ]... [ *FILE* ]... + +* DESCRIPTION + +** HLS Options: + +- --no-hls :: Do not use HLS and generate standard flow +- --simulate :: Simulate the result with the Verilog semantics +- --debug-hls :: Add debug logic to the Verilog +- --initialise-stack :: initialise the stack to all 0s + +** HLS Optimisations: + +- -fschedule :: Schedule the resulting hardware [off] +- -fif-conversion :: If-conversion optimisation [off] + +** General options: + +- -stdlib :: Set the path of the Compcert run-time library +- -v :: Print external commands before invoking them +- -timings :: Show the time spent in various compiler passes +- -version :: Print the version string and exit +- -target :: Generate code for the given target +- -conf :: Read configuration from file +- @ :: Read command line options from + +** Tracing Options: + +- -dprepro :: Save C file after preprocessing in .i +- -dparse :: Save C file after parsing and elaboration in .parsed.c +- -dc :: Save generated C in .compcert.c +- -dclight :: Save generated Clight in .light.c +- -dcminor :: Save generated Cminor in .cm +- -drtl :: Save RTL at various optimization points in .rtl. +- -drtlblock :: Save RTLBlock .rtlblock +- -dhtl :: Save HTL before Verilog generation .htl +- -dltl :: Save LTL after register allocation in .ltl +- -dmach :: Save generated Mach code in .mach +- -dasm :: Save generated assembly in .s +- -dall :: Save all generated intermediate files in . +- -sdump :: Save info for post-linking validation in .json +- -o :: Generate output in + +** Diagnostic options: + +- -Wall :: Enable all warnings +- -W :: Enable the specific +- -Wno- :: Disable the specific +- -Werror :: Make all warnings into errors +- -Werror= :: Turn into an error +- -Wno-error= :: Turn into a warning even if -Werror is specified +- -Wfatal-errors :: Turn all errors into fatal errors aborting the compilation +- -fdiagnostics-color :: Turn on colored diagnostics +- -fno-diagnostics-color :: Turn of colored diagnostics +- -fmax-errors= :: Maximum number of errors to report +- -fdiagnostics-show-option :: Print the option name with mappable diagnostics +- -fno-diagnostics-show-option :: Turn of printing of options with mappable diagnostics + +* AUTHOR + +Written by Yann Herklotz, Michalis Pardalos, James Pollard, Nadesh Ramanathan and John Wickerson. + +* COPYRIGHT + +Copyright (C) 2019-2022 Yann Herklotz + +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 . diff --git a/doc/res/coqdoc.css b/doc/res/coqdoc.css new file mode 100644 index 0000000..5572aaa --- /dev/null +++ b/doc/res/coqdoc.css @@ -0,0 +1,867 @@ +body { + padding: 0px 0px; + margin: 0px 0px; + padding-left: 1em; + background-color: white; + font-family: sans-serif; + background-repeat: no-repeat; + background-size: 100%; +} + +#page { + display: block; + padding: 0px; + margin: 0px; +} + +#header { + min-height: 100px; + max-width: 760px; + margin: 0 auto; + padding-left: 80px; + padding-right: 80px; + padding-top: 30px; +} + +#header h1 { + padding: 0; + margin: 0; +} + +/* Menu */ +ul#menu { + padding: 0; + display: block; + margin: auto; +} + +ul#menu li, div.button { + display: inline-block; + background-color: white; + padding: 5px; + font-size: .70em; + text-transform: uppercase; + width: 30%; + text-align: center; + font-weight: 600; +} + +div.button { + margin-top:5px; + width: 40%; +} + +#button_block {margin-top:50px;} + +ul#menu a.hover li { + background-color: red; +} + +/* Contents */ + +#main, #main_home { + display: block; + padding: 80px; + padding-top: 60px; /* BCP */ + font-size: 100%; + line-height: 100%; + max-width: 760px; + background-color: #ffffff; + margin: 0 auto; +} + +#main_home { + background-color: rgba(255, 255, 255, 0.5); +} + +#index_content div.intro p { + font-size: 12px; +} + +#main h1 { + /* line-height: 80%; */ + line-height: normal; + padding-top: 3px; + padding-bottom: 4px; + /* Demitri: font-size: 22pt; */ + font-size: 200%; /* BCP */ +} + +/* allow for multi-line headers */ +#main a.idref:visited {color : #416DFF; text-decoration : none; } +#main a.idref:link {color : #416DFF; text-decoration : none; } +#main a.idref:hover {text-decoration : none; } +#main a.idref:active {text-decoration : none; } + +#main a.modref:visited {color : #416DFF; text-decoration : none; } +#main a.modref:link {color : #416DFF; text-decoration : none; } +#main a.modref:hover {text-decoration : none; } +#main a.modref:active {text-decoration : none; } + +#main .keyword { color : #697f2f } +#main { color: black } + +/* General section class - applies to all .section IDs */ +.section { + padding-top: 12px; + padding-bottom: 11px; + padding-left: 8px; + margin-top: 5px; + margin-bottom: 3px; + margin-top: 18px; + font-size : 125%; + color: #ffffff; +} + +/* Book title in header */ +.booktitleinheader { + color: #000000; + text-transform: uppercase; + font-weight: 300; + letter-spacing: 1px; + font-size: 125%; + margin-left: 0px; + margin-bottom: 22px; + } + +/* Chapter titles */ +.libtitle { + max-width: 860px; + text-transform: uppercase; + margin: 5px auto; + font-weight: 500; + padding-bottom: 2px; + font-size: 120%; + letter-spacing: 3px; + } + +.subtitle { + display: block; + padding-top: 10px; + font-size: 70%; + line-height: normal; +} + +h2.section { + color: #2a2c71; + background-color: transparent; + padding-left: 0px; + padding-top: 0px; + padding-bottom: 0px; + /* margin-top: 0px; */ + margin-top: 9px; /* BCP 2/20 */ + font-size : 135%; } + +h3.section { + /* background-color: rgb(90%,90%,100%); */ + background-color: white; + /* padding-left: 8px; */ + padding-left: 0px; + /* padding-top: 7px; */ + padding-top: 0px; + /* padding-bottom: 0px; */ + padding-bottom: 0.5em; + /* margin-top: 9px; */ + /* margin-top: 4px; (BCP 2/20) */ + margin-top: 9px; /* BCP 2/20 */ + font-size : 115%; + color:black; +} + +h4.section { + margin-top: .2em; + background-color: white; + color: #2a2c71; + padding-left: 0px; + padding-top: 0px; + padding-bottom: 0.5em; /* 0px; */ + font-size : 100%; + font-style : bold; + text-decoration : underline; +} + +#header p { + font-size: 13px; +} + +/* Sets up Main ID and margins */ + +#main .doc { + margin: 0px auto; + font-size: 14px; + line-height: 22px; + /* max-width: 570px; */ + color: black; + /* text-align: justify; */ + border-style: plain; + /* This might work better after changing back to standard coqdoc: */ + padding-top: 10px; + /* padding-top: 18px; */ +} + +.quote { + margin-left: auto; + margin-right: auto; + width: 40em; + color: darkred; +} + +.loud { + color: darkred; +} + +pre { + margin-top: 0px; + margin-bottom: 0px; +} + +.inlinecode { + display: inline; + /* font-size: 125%; */ + color: #444444; + font-family: monospace } + +.doc .inlinecode { + display: inline; + font-size: 105%; + color: rgb(35%,35%,70%); + font-family: monospace } + +.doc .inlinecode .id { +/* I am changing this to white in style below: + color: rgb(35%,35%,70%); +*/ +} + +h1 .inlinecode .id, h1.section span.inlinecode { + color: #ffffff; +} + +.inlinecodenm { + display: inline; + /* font-size: 125%; */ + color: #444444; +} + +.doc .inlinecodenm { + display: inline; + color: rgb(35%,35%,70%); +} + +.doc .inlinecodenm .id { + color: rgb(35%,35%,70%); +} + +.doc .code { + display: inline; + font-size: 110%; + color: rgb(35%,35%,70%); + font-family: monospace; + padding-left: 0px; +} + +.comment { + display: inline; + font-family: monospace; + color: rgb(50%,50%,80%); +} + +.inlineref { + display: inline; + /* font-family: monospace; */ + color: rgb(50%,50%,80%); +} + +.show::before { + /* content: "more"; */ + content: "+"; +} + +.show { + background-color: rgb(93%,93%,93%); + display: inline; + font-family: monospace; + font-size: 60%; + padding-top: 1px; + padding-bottom: 2px; + padding-left: 4px; + padding-right: 4px; + color: rgb(60%,60%,60%); +} + +/* +.show { + display: inline; + font-family: monospace; + font-size: 60%; + padding-top: 0px; + padding-bottom: 0px; + padding-left: 10px; + border: 1px; + border-style: solid; + color: rgb(75%,75%,85%); +} +*/ + +.proofbox { + font-size: 90%; + color: rgb(75%,75%,75%); +} + +#main .less-space { + margin-top: -12px; +} + +/* Inline quizzes */ +.quiz:before { + color: rgb(40%,40%,40%); + /* content: "- Quick Check -" ; */ + display: block; + text-align: center; + margin-bottom: 5px; +} +.quiz { + border: 4px; + border-color: rgb(80%,80%,80%); + /* + margin-left: 40px; + margin-right: 100px; + */ + padding: 5px; + padding-left: 8px; + padding-right: 8px; + margin-top: 10px; + margin-bottom: 15px; + border-style: solid; +} + +/* For textual ones... */ +.show-old { + display: inline; + font-family: monospace; + font-size: 80%; + padding-top: 0px; + padding-bottom: 0px; + padding-left: 3px; + padding-right: 3px; + border: 1px; + margin-top: 5px; /* doesn't work?! */ + border-style: solid; + color: rgb(75%,75%,85%); +} + +.largebr { + margin-top: 10px; +} + +.code { + padding-left: 20px; + font-size: 14px; + font-family: monospace; + line-height: 17px; + margin-top: 9px; +} + +/* Working: +.code { + display: block; + padding-left: 0px; + font-size: 110%; + font-family: monospace; + } +*/ + +.code-space { + max-width: 50em; + margin-top: 0em; + /* margin-bottom: -.5em; */ + margin-left: auto; + margin-right: auto; +} + +.code-tight { + max-width: 50em; + margin-top: .6em; + /* margin-bottom: -.7em; */ + margin-left: auto; + margin-right: auto; +} + +hr.doublespaceincode { + height: 1pt; + visibility: hidden; + font-size: 10px; +} + +/* +code.br { + height: 5em; +} +*/ + +#main .citation { + color: rgb(70%,0%,0%); + text-decoration: underline; +} + +table.infrule { + border: 0px; + margin-left: 50px; + margin-top: .5em; + margin-bottom: 1.2em; +} + +td.infrule { + font-family: monospace; + text-align: center; + /* color: rgb(35%,35%,70%); */ + padding: 0px; + line-height: 100%; +} + +tr.infrulemiddle hr { + margin: 1px 0 1px 0; +} + +.infrulenamecol { + color: rgb(60%,60%,60%); + font-size: 80%; + padding-left: 1em; + padding-bottom: 0.1em +} + +#footer { + font-size: 65%; + font-family: sans-serif; +} + +.id { display: inline; } + +.id[title="constructor"] { + color: #697f2f; +} + +.id[title="var"], +.id[title="variable"] { + color: rgb(40%,0%,40%); +} + +.id[title="definition"] { + color: rgb(0%,40%,0%); +} + +.id[title="abbreviation"] { + color: rgb(0%,40%,0%); +} + +.id[title="lemma"] { + color: rgb(0%,40%,0%); +} + +.id[title="instance"] { + color: rgb(0%,40%,0%); +} + +.id[title="projection"] { + color: rgb(0%,40%,0%); +} + +.id[title="method"] { + color: rgb(0%,40%,0%); +} + +.id[title="inductive"] { + color: #034764; +} + +.id[title="record"] { + color: rgb(0%,0%,80%); +} + +.id[title="class"] { + color: rgb(0%,0%,80%); +} + +.id[title="keyword"] { + color : #697f2f; + /* color: black; */ +} + +.inlinecode .id { + color: rgb(0%,0%,0%); +} + +.nowrap { + white-space: nowrap; +} + +.HIDEFROMHTML { + display: none; +} + +/* TOC */ + +#toc h2 { +/* padding-top: 13px; */ + padding-bottom: 13px; + padding-left: 8px; + margin-top: 5px; + margin-top: 20px; + /* OLD: padding: 10px; + line-height: 120%; + background-color: rgb(60%,60%,100%); */ +} + +#toc h2.ui-accordion-header { + padding: .5em .5em .5em .7em; + outline: none; +} + +#toc .ui-accordion .ui-accordion-content { + padding: 0.5em 2.5em 0.8em .9em; + border-top: 0; + margin-bottom: 1em; + /* bottom rule */ + border: none; + border-bottom: 1px solid transparent; + transition: border-bottom-color 0.25s ease-in; + transition-delay: 0.15s; +} + +#toc .ui-accordion .ui-accordion-content-active { + border-bottom: 1px solid #9b9b9b; + transition-delay: 0s; +} + +#toc h2.ui-accordion-header-active { + background: silver !important; +} + +#toc h2:not(.ui-accordion-header-active):hover { + background: rgba(0,0,0,0.04) !important; +} + +#toc h2 a:hover { + text-decoration: underline; +} + +#toc h2:hover::after { + content: "expand ▾"; + font-size: 80%; + float: right; + margin-top: 0.2em; + color: silver; + opacity: 1; + transition: opacity .5s ease-in-out; +} + +#toc h2.ui-accordion-header-active:hover::after { + opacity: 0; +} + +#toc h2 .select { background-image: url('media/image/arrow_down.jpg'); } +div#sec1.hide { display: none; } + +#toc ul { + padding-top: 8px; + font-size: 14px; + padding-left: 0; +} + +#toc ul ul { + margin-bottom: -8px; +} + +#toc li { + font-weight: 600; + list-style-type: none; + padding-top: 12px; + padding-bottom: 8px; +} + +#toc li li { + font-weight: 300; + list-style-type: circle; + padding-bottom: 3px; + padding-top: 0px; + margin-left: 19px; +} + + + + +/* Accordion Overrides */ + +/* Widget Bar */ +.ui-state-default, +.ui-widget-content .ui-state-default, +.ui-widget-header .ui-state-default, +.ui-button, +/* We use html here because we need a greater specificity to make sure disabled + works properly when clicked or hovered */ +html .ui-button.ui-state-disabled:hover, +html .ui-button.ui-state-disabled:active { + border: none!important; + /* BCP 3/17: I like it better without the rules... + border-bottom: 1px solid silver!important; */ + background: white !important; + font-weight: normal; + color: #454545!important; + font-weight: 400!important; + margin-top: 0px!important; + +} + +/* Misc visuals +----------------------------------*/ + +/* Corner radius */ +.ui-corner-all, +.ui-corner-top, +.ui-corner-left, +.ui-corner-tl { + border-top-left-radius: 0px!important; +} + +.ui-corner-all, +.ui-corner-top, +.ui-corner-right, +.ui-corner-tr { + border-top-right-radius: 0px!important; +} + +.ui-corner-all, +.ui-corner-bottom, +.ui-corner-left, +.ui-corner-bl { + border-bottom-left-radius: 0px!important; +} + +.ui-corner-all, +.ui-corner-bottom, +.ui-corner-right, +.ui-corner-br { + border-bottom-right-radius: 0px!important; +} + +html .ui-button.ui-state-disabled:focus { + color: red!important; +} + +/* Remove Icon */ +.ui-icon { display: none!important; } + +/* Widget */ +.ui-widget-content { + border: 1px solid #9e9e9e; + border-bottom-color: #b2b2b2; +} + +.ui-widget-content { + background: #ffffff; + color: #333333; +} + + +/* Index */ + +#index { + margin: 0; + padding: 0; + width: 100%; + font-style : normal; +} + +#index #frontispiece { + margin: auto; + padding: 1em; + width: 700px; +} + +.booktitle { + font-size : 300%; line-height: 100%; font-style:bold; + color: white; + padding-top: 70px; + padding-bottom: 20px; } +.authors { font-size : 200%; + line-height: 115%; } +.moreauthors { font-size : 170% } +.buttons { font-size : 170%; + margin-left: auto; + margin-right: auto; + font-style : bold; + } + +/* Link colors never changes */ + +A:link, A:visited, A:active, A:hover { + text-decoration: none; + color: #555555 +} + +/* Special color for the chapter header */ + +.booktitleinheader A:visited, .booktitleinheader A:active, .booktitleinheader A:hover, .booktitleinheader A:link { + text-decoration: none; + color: black; +} + +#index #entrance { + text-align: center; +} + +/* This was removed via CSS but the HTML is still generated */ +#index #footer { + display: none; +} + +.paragraph { + height: 0.6em; +} + +ul.doclist { + margin-top: 0em; + margin-bottom: 0em; +} + +/* Index styles */ + +/* Styles the author box (Intro class) and With (column class) */ + +.column { + float:left; + width: 43%; + margin:0 10px; + text-align: left; + font-size: 15px; + line-height: 25px; + padding-right: 20px; + min-height: 340px; +} + +.smallauthors { + font-size: 19px; + line-height: 25px; +} + +.mediumauthors { + font-size: 23px; + line-height: 33px; +} + +.largeauthors { + font-size: 28px; + line-height: 40px; +} + +.intro { + width: 35%; + font-size: 21px; + line-height: 27px; + font-weight: 600; + padding-right: 20px; +} + +.column.pub { + width: 40%; + margin-bottom: 20px; +} + +#index_content { + width: 100%!important; + display: block; + min-height: 400px; +} + +div.column.pub table tbody tr td { + text-align: center; padding: 10px; +} +div.column.pub table tbody tr td p { + text-align: left; + margin-top: 0; + font-weight: 600; + font-size: 13px!important; + line-height: 18px; +} + +/* Tables */ + +td.tab { + height: 16px; + font-weight: 600; + padding-left: 5px; + text-align: left!important; +} + +/* Styles tables on the index -- body class sf_home is used there */ + +body.sf_home table { + min-height: 450px; + vertical-align: top; +} + +body.sf_home table td { + vertical-align: top; + +} +body.sf_home table td p { + min-height: 100px; + +} + +table.logical { background-color: rgba(144, 160, 209, 0.5); } +table.logical tbody tr td.tab { background-color: #91a1d1; } + +table.language_found { background-color: rgba(178, 88, 88, 0.5); } +table.language_found tbody tr td.tab { background-color: #b25959; } + +table.algo { background-color: rgba(194, 194, 108, 0.5); } +table.algo tbody tr td.tab { background-color: #c2c26c; } + +table.qc { background-color: rgba(185, 170, 185, 0.5); } +table.qc tbody tr td.tab { background-color: #8b7d95; } + +table.vc { background-color: rgba(159, 125, 140, 0.5); } +table.vc tbody tr td.tab { background-color: rgb(159, 125, 140); } + +table.slf { background-color: rgba(219, 178, 127, 0.5); } +table.slf tbody tr td.tab { background-color: rgb(219, 178, 127); } + +/* Suggested background color for next volume */ +/* #c07d62 */ + +.ui-draggable, .ui-droppable { + background-position: top; +} + +/* Chapter dependencies (SVG) */ +.deps a polygon:hover { opacity: 0.6; stroke-width: 2; } +.deps a text { pointer-events: none; } + +/* A few specific things for the top-level SF landing page */ + +body.sf_home {background-color: #ededed; background-image: url(../media/image/core_mem_bg.jpg); } + +body.sf_home #header { + background-image: url(../media/image/core_mem_hdr_bg.jpg); + padding-bottom: 20px; +} + +body.sf_home #main_home { + background-color: transparent; +} + +/* A partial fix to a coqdoc bug... + See https://github.com/DeepSpec/sfdev/issues/236 */ +.inlinecode { white-space: pre; } +.inlinecode br { display: none; } + +#header { background-color: rgba(190, 170, 190, 0.5); } + +/* This volume's color */ +.section, ul#menu li.section_name, div.button { background-color: #8b7d95; } + +.slide img { + border: 2px solid gray; + margin: 1em; +} diff --git a/doc/res/fdl.org b/doc/res/fdl.org new file mode 100644 index 0000000..81e2cd9 --- /dev/null +++ b/doc/res/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/doc/res/install-deps.el b/doc/res/install-deps.el new file mode 100644 index 0000000..09cf4ae --- /dev/null +++ b/doc/res/install-deps.el @@ -0,0 +1,11 @@ +(require 'package) +(package-initialize) +(add-to-list 'package-archives '("nongnu" . "https://elpa.nongnu.org/nongnu/") t) +(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t) +(add-to-list 'package-archives '("gnu-devel" . "https://elpa.gnu.org/devel/") t) +(package-refresh-contents) + +(package-install 'org) +(package-install 'org-contrib) +(package-install 'org-transclusion) +(package-install 'htmlize) diff --git a/doc/res/publish.el b/doc/res/publish.el new file mode 100644 index 0000000..c083eb0 --- /dev/null +++ b/doc/res/publish.el @@ -0,0 +1,23 @@ +(require 'package) +(package-initialize) + +(require 'org) +(require 'org-transclusion) +(require 'ox) +(require 'ox-html) +(require 'htmlize) +(require 'ox-texinfo) +(require 'ox-man) + +(setq org-transclusion-exclude-elements nil + org-html-head-include-default-style nil + org-html-head-include-scripts nil + org-html-postamble-format '(("en" "")) + org-html-postamble t + org-html-divs '((preamble "header" "header") + (content "article" "content") + (postamble "footer" "postamble")) + org-html-doctype "html5" + org-html-htmlize-output-type 'css) + +(org-transclusion-add-all) diff --git a/doc/vericert.rst b/doc/vericert.rst new file mode 100644 index 0000000..3c8eaeb --- /dev/null +++ b/doc/vericert.rst @@ -0,0 +1,530 @@ +=============== +Vericert Manual +=============== + + +Introduction +------------ + +Vericert translates C code into a hardware description language called Verilog, which can then be +synthesised into hardware, to be placed onto a field-programmable gate array (FPGA) or +application-specific integrated circuit (ASIC). + +.. _fig:design: + +.. figure:: /_static/images/toolflow.png + + Current design of Vericert, where HTL is an intermediate language representing a finite state + machine with data-path (FSMD) and Verilog is the target language. + +The design shown in Figure `fig:design`_ shows how Vericert leverages an existing verified C +compiler called `CompCert `_ to perform this translation. + +.. index:: vericert + +.. _building: + +Building Vericert +----------------- + + +Testing +~~~~~~~ + +To test out ``vericert`` you can try the following examples which are in the test folder using the +following: + +.. code:: shell + + ./bin/vericert test/loop.c -o loop.v + ./bin/vericert test/conditional.c -o conditional.v + ./bin/vericert test/add.c -o add.v + +Or by running the test suite using the following command: + +.. code:: shell + + make test + +.. _using-vericert: + +.. index:: vericert + +Using Vericert +-------------- + +Vericert can be used to translate a subset of C into Verilog. As a simple example, consider the +following C file (``main.c``): + +.. code:: C + + void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) { + int sum = 0; + for (int c = 0; c < 2; c++) { + for (int d = 0; d < 2; d++) { + for (int k = 0; k < 2; k++) { + sum = sum + first[c][k]*second[k][d]; + } + multiply[c][d] = sum; + sum = 0; + } + } + } + + int main() { + int f[2][2] = {{1, 2}, {3, 4}}; + int s[2][2] = {{5, 6}, {7, 8}}; + int m[2][2] = {{0, 0}, {0, 0}}; + + matrix_multiply(f, s, m); + return m[1][1]; + } + +It can be compiled using the following command, assuming that vericert is somewhere on the path. + +.. code:: shell + + vericert main.c -o main.v + +The Verilog file contains a top-level test-bench, which can be given to any Verilog simulator to +simulate the hardware, which should give the same result as executing the C code. Using `Icarus +Verilog `_ as an example: + +.. code:: shell + + iverilog -o main_v main.v + +When executing, it should therefore print the following: + +.. code:: shell + + $ ./main_v + finished: 50 + +This gives the same result as executing the C in the following way: + +.. code:: shell + + $ gcc -o main_c main.c + $ ./main_c + $ echo $? + 50 + +Man pages +~~~~~~~~~ + +.. _unreleased-features: + +Unreleased Features +------------------- + +The following are unreleased features in Vericert that are currently being worked on and have not +been completely proven correct yet. Currently this includes features such as: + +- `scheduling`_, + +- `operation-chaining`_, + +- `if-conversion`_, and + +- `functions`_. + +This page gives some preliminary information on how the features are implemented and how the proofs +for the features are being done. Once these features are properly implemented, they will be added +to the proper documentation. + +.. _scheduling: + +Scheduling +~~~~~~~~~~ + +Scheduling is an optimisation which is used to run various instructions in parallel that are +independent to each other. + +.. _operation-chaining: + +Operation Chaining +~~~~~~~~~~~~~~~~~~ + +Operation chaining is an optimisation that can be added on to scheduling and allows for the +sequential execution of instructions in a clock cycle, while executing other instructions in +parallel in the same clock cycle. + +.. _if-conversion: + +If-conversion +~~~~~~~~~~~~~ + +If-conversion is an optimisation which can turn code with simple control flow into a single block +(called a hyper-block), using predicated instructions. + +.. _functions: + +Functions +~~~~~~~~~ + +Functions are currently only inlined in Vericert, however, we are working on a proper interface to +integrate function calls into the hardware. + +.. _coq-style-guide: + +Coq Style Guide +--------------- + +This style guide was taken from `Silveroak `_, it outlines +code style for Coq code in this repository. There are certainly other valid strategies and opinions +on Coq code style; this is laid out purely in the name of consistency. For a visual example of the +style, see the `example`_ at the bottom of this file. + +.. _code-organization: + +Code organization +~~~~~~~~~~~~~~~~~ + +.. _legal-banner: + +Legal banner +^^^^^^^^^^^^ + +- Files should begin with a copyright/license banner, as shown in the example above. + +.. _import-statements: + +Import statements +^^^^^^^^^^^^^^^^^ + +- ``Require Import`` statements should all go at the top of the file, followed by file-wide ``Import`` + statements. + + - =Import=s often contain notations or typeclass instances that might override notations or + instances from another library, so it’s nice to highlight them separately. + +- One ``Require Import`` statement per line; it’s easier to scan that way. + +- ``Require Import`` statements should use “fully-qualified” names (e.g. ``Require Import + Coq.ZArith.ZArith`` instead of ``Require Import ZArith``). + + - Use the ``Locate`` command to find the fully-qualified name! + +- ``Require Import``’s should go in the following order: + + 1. Standard library dependencies (start with ``Coq.``) + + 2. External dependencies (anything outside the current project) + + 3. Same-project dependencies + +- ``Require Import``’s with the same root library (the name before the first ``.``) should be + grouped together. Within each root-library group, they should be in alphabetical order (so + ``Coq.Lists.List`` before ``Coq.ZArith.ZArith``). + +.. _notations-and-scopes: + +Notations and scopes +^^^^^^^^^^^^^^^^^^^^ + +- Any file-wide ``Local Open Scope``’s should come immediately after the =Import=s (see example). + + - Always use ``Local Open Scope``; just ``Open Scope`` will sneakily open the scope for those who + import your file. + +- Put notations in their own separate modules or files, so that those who import your file can + choose whether or not they want the notations. + + - Conflicting notations can cause a lot of headache, so it comes in very handy to leave this + flexibility! + +.. _formatting: + +Formatting +~~~~~~~~~~ + +.. _line-length: + +Line length +^^^^^^^^^^^ + +- Maximum line length 80 characters. + + - Many Coq IDE setups divide the screen in half vertically and use only half to display source + code, so more than 80 characters can be genuinely hard to read on a laptop. + +.. _whitespace-and-indentation: + +Whitespace and indentation +^^^^^^^^^^^^^^^^^^^^^^^^^^ + +- No trailing whitespace. + +- Spaces, not tabs. + +- Files should end with a newline. + + - Many editors do this automatically on save. + +- Colons may be either “English-spaced”, with no space before the colon and one space after (``x: + nat``) or “French-spaced”, with one space before and after (``x : nat``). + +- Default indentation is 2 spaces. + + - Keeping this small prevents complex proofs from being indented ridiculously far, and matches IDE + defaults. + +- Use 2-space indents if inserting a line break immediately after: + + - ``Proof.`` + + - ``fun <...> =>`` + + - ``forall <...>,`` + + - ``exists <....>,`` + +- The style for indenting arguments in function application depends on where you make a line + break. If you make the line break immediately after the function name, use a 2-space + indent. However, if you make it after one or more arguments, align the next line with the first + argument: + + .. code:: coq + + (Z.pow + 1 2) + (Z.pow 1 2 3 + 4 5 6) + +- ``Inductive`` cases should not be indented. Example: + + .. code:: coq + + Inductive Foo : Type := + | FooA : Foo + | FooB : Foo + . + +- ``match`` or ``lazymatch`` cases should line up with the “m” in ``match`` or “l” in ``lazymatch``, + as in the following examples: + + .. code:: coq + + match x with + | 3 => true + | _ => false + end. + + lazymatch x with + | 3 => idtac + | _ => fail "Not equal to 3:" x + end. + + repeat match goal with + | _ => progress subst + | _ => reflexivity + end. + + do 2 lazymatch goal with + | |- context [eq] => idtac + end. + +.. _definitions-and-fixpoints: + +Definitions and Fixpoints +~~~~~~~~~~~~~~~~~~~~~~~~~ + +- It’s okay to leave the return type of ``Definition``’s and ``Fixpoint``’s implicit + (e.g. ``Definition x := 5`` instead of ``Definition x : nat := 5``) when the type is very simple + or obvious (for instance, the definition is in a file which deals exclusively with operations on + ``Z``). + +.. _inductives: + +Inductives +~~~~~~~~~~ + +- The ``.`` ending an ``Inductive`` can be either on the same line as the last case or on its own + line immediately below. That is, both of the following are acceptable: + + .. code:: coq + + Inductive Foo : Type := + | FooA : Foo + | FooB : Foo + . + Inductive Foo : Type := + | FooA : Foo + | FooB : Foo. + +.. _lemmatheorem-statements: + +Lemma/Theorem statements +~~~~~~~~~~~~~~~~~~~~~~~~ + +- Generally, use ``Theorem`` for the most important, top-level facts you prove and ``Lemma`` for + everything else. + +- Insert a line break after the colon in the lemma statement. + +- Insert a line break after the comma for ``forall`` or ``exist`` quantifiers. + +- Implication arrows (``->``) should share a line with the previous hypothesis, not the following + one. + +- There is no need to make a line break after every ``->``; short preconditions may share a line. + +.. _proofs-and-tactics: + +Proofs and tactics +~~~~~~~~~~~~~~~~~~ + +- Use the ``Proof`` command (lined up vertically with ``Lemma`` or ``Theorem`` it corresponds to) to + open a proof, and indent the first line after it 2 spaces. + +- Very small proofs (where ``Proof. 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 ``_step``, + because the single-step version is much easier to debug. For instance: + + .. code:: coq + + Ltac crush_step := + match goal with + | _ => progress subst + | _ => reflexivity + end. + Ltac crush := repeat crush_step. + +.. _naming: + +Naming +~~~~~~ + +- Helper proofs about standard library datatypes should go in a module that is named to match the + standard library module (see example). + + - This makes the helper proofs look like standard-library ones, which is helpful for categorizing + them if they’re genuinely at the standard-library level of abstraction. + +- Names of modules should start with capital letters. + +- Names of inductives and their constructors should start with capital letters. + +- Names of other definitions/lemmas should be snake case. + +.. _example: + +Example +~~~~~~~ + +A small standalone Coq file that exhibits many of the style points. + +.. code:: coq + + (* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2021 Name + * + * + *) + + Require Import Coq.Lists.List. + Require Import Coq.micromega.Lia. + Require Import Coq.ZArith.ZArith. + Import ListNotations. + Local Open Scope Z_scope. + + (* Helper proofs about standard library integers (Z) go within [Module Z] so + that they match standard-library Z lemmas when used. *) + Module Z. + Lemma pow_3_r x : x ^ 3 = x * x * x. + Proof. lia. Qed. (* very short proofs can go all on one line *) + + Lemma pow_4_r x : x ^ 4 = x * x * x * x. + Proof. + change 4 with (Z.succ (Z.succ (Z.succ (Z.succ 0)))). + repeat match goal with + | _ => rewrite Z.pow_1_r + | _ => rewrite Z.pow_succ_r by lia + | |- context [x * (?a * ?b)] => + replace (x * (a * b)) with (a * b * x) by lia + | _ => reflexivity + end. + Qed. + End Z. + (* Now we can access the lemmas above as Z.pow_3_r and Z.pow_4_r, as if they + were in the ZArith library! *) + + Definition bar (x y : Z) := x ^ (y + 1). + + (* example with a painfully manual proof to show case formatting *) + Lemma bar_upper_bound : + forall x y a, + 0 <= x <= a -> 0 <= y -> + 0 <= bar x y <= a ^ (y + 1). + Proof. + (* avoid referencing autogenerated names by explicitly naming variables *) + intros x y a Hx Hy. revert y Hy x a Hx. + (* explicitly indicate # subgoals with [ | ... | ] if > 1 *) + cbv [bar]; refine (natlike_ind _ _ _); [ | ]. + { (* y = 0 *) + intros; lia. } + { (* y = Z.succ _ *) + intros. + rewrite Z.add_succ_l, Z.pow_succ_r by lia. + split. + { (* 0 <= bar x y *) + apply Z.mul_nonneg_nonneg; [ lia | ]. + apply Z.pow_nonneg; lia. } + { (* bar x y < a ^ y *) + rewrite Z.pow_succ_r by lia. + apply Z.mul_le_mono_nonneg; try lia; + [ apply Z.pow_nonneg; lia | ]. + (* For more flexible proofs, use match statements to find hypotheses + rather than referring to them by autogenerated names like H0. In this + case, we'll take any hypothesis that applies to and then solves the + goal. *) + match goal with H : _ |- _ => apply H; solve [auto] end. } } + Qed. + + (* Put notations in a separate module or file so that importers can + decide whether or not to use them. *) + Module BarNotations. + Infix "#" := bar (at level 40) : Z_scope. + Notation "x '##'" := (bar x x) (at level 40) : Z_scope. + End BarNotations. diff --git a/docs/Makefile b/docs/Makefile deleted file mode 100644 index 9d4f361..0000000 --- a/docs/Makefile +++ /dev/null @@ -1,39 +0,0 @@ -all: manual src man-html - -install-deps: - emacs --batch --load ./res/install-deps.el - -%.man: %.org - emacs --batch --file $< --load ./res/publish.el --funcall org-man-export-to-man - -%.html: %.org - emacs --batch --file $< --load ./res/publish.el --funcall org-html-export-to-html - -manual: - mkdir -p manual - emacs --batch --file documentation.org --load ./res/publish.el --funcall org-texinfo-export-to-texinfo - 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/. - -man-html: man.html - mkdir -p man - cp man.html ./man/vericert.1.html - -vericert.1: man.man - cp $< $@ - -src: - $(MAKE) -C .. doc - cp -r ../html src - -upload: - tar caf docs.tar.xz manual man src - rsync docs.tar.xz "zk@leika.ymhg.org:~" - -.PHONY: all upload manual man src install-deps man-html - -clean: - rm -rf manual man src - rm -f docs.tar.xz diff --git a/docs/README.org b/docs/README.org deleted file mode 100644 index 4113ed9..0000000 --- a/docs/README.org +++ /dev/null @@ -1,7 +0,0 @@ -#+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 deleted file mode 100644 index aa27264..0000000 --- a/docs/common.org +++ /dev/null @@ -1,15 +0,0 @@ -#+author: Yann Herklotz -#+email: git@ymhg.org - -#+macro: version 1.2.2 -#+macro: modified 2022-02-24 - -#+macro: base_url https://vericert.ymhg.org - -#+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 deleted file mode 100644 index 85bc8fd..0000000 --- a/docs/documentation.org +++ /dev/null @@ -1,562 +0,0 @@ -#+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. 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 =_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 - * - * - *) - - 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 diff --git a/docs/images/toolflow.pdf b/docs/images/toolflow.pdf deleted file mode 100644 index 5fcee67..0000000 Binary files a/docs/images/toolflow.pdf and /dev/null differ diff --git a/docs/images/toolflow.png b/docs/images/toolflow.png deleted file mode 100644 index 601d6be..0000000 Binary files a/docs/images/toolflow.png and /dev/null differ diff --git a/docs/images/toolflow.svg b/docs/images/toolflow.svg deleted file mode 100644 index 0d8f39f..0000000 --- a/docs/images/toolflow.svg +++ /dev/null @@ -1,1250 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/docs/man.org b/docs/man.org deleted file mode 100644 index cb6143f..0000000 --- a/docs/man.org +++ /dev/null @@ -1,89 +0,0 @@ -#+title: vericert -#+man_class_options: :section-id "1" -#+options: toc:nil num:nil -#+html_head_extra: - -* NAME - -vericert - A formally verified high-level synthesis tool. - -* SYNOPSYS - -*vericert* [ *OPTION* ]... [ *FILE* ]... - -* DESCRIPTION - -** HLS Options: - -- --no-hls :: Do not use HLS and generate standard flow -- --simulate :: Simulate the result with the Verilog semantics -- --debug-hls :: Add debug logic to the Verilog -- --initialise-stack :: initialise the stack to all 0s - -** HLS Optimisations: - -- -fschedule :: Schedule the resulting hardware [off] -- -fif-conversion :: If-conversion optimisation [off] - -** General options: - -- -stdlib :: Set the path of the Compcert run-time library -- -v :: Print external commands before invoking them -- -timings :: Show the time spent in various compiler passes -- -version :: Print the version string and exit -- -target :: Generate code for the given target -- -conf :: Read configuration from file -- @ :: Read command line options from - -** Tracing Options: - -- -dprepro :: Save C file after preprocessing in .i -- -dparse :: Save C file after parsing and elaboration in .parsed.c -- -dc :: Save generated C in .compcert.c -- -dclight :: Save generated Clight in .light.c -- -dcminor :: Save generated Cminor in .cm -- -drtl :: Save RTL at various optimization points in .rtl. -- -drtlblock :: Save RTLBlock .rtlblock -- -dhtl :: Save HTL before Verilog generation .htl -- -dltl :: Save LTL after register allocation in .ltl -- -dmach :: Save generated Mach code in .mach -- -dasm :: Save generated assembly in .s -- -dall :: Save all generated intermediate files in . -- -sdump :: Save info for post-linking validation in .json -- -o :: Generate output in - -** Diagnostic options: - -- -Wall :: Enable all warnings -- -W :: Enable the specific -- -Wno- :: Disable the specific -- -Werror :: Make all warnings into errors -- -Werror= :: Turn into an error -- -Wno-error= :: Turn into a warning even if -Werror is specified -- -Wfatal-errors :: Turn all errors into fatal errors aborting the compilation -- -fdiagnostics-color :: Turn on colored diagnostics -- -fno-diagnostics-color :: Turn of colored diagnostics -- -fmax-errors= :: Maximum number of errors to report -- -fdiagnostics-show-option :: Print the option name with mappable diagnostics -- -fno-diagnostics-show-option :: Turn of printing of options with mappable diagnostics - -* AUTHOR - -Written by Yann Herklotz, Michalis Pardalos, James Pollard, Nadesh Ramanathan and John Wickerson. - -* COPYRIGHT - -Copyright (C) 2019-2022 Yann Herklotz - -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 . diff --git a/docs/res/coqdoc.css b/docs/res/coqdoc.css deleted file mode 100644 index 5572aaa..0000000 --- a/docs/res/coqdoc.css +++ /dev/null @@ -1,867 +0,0 @@ -body { - padding: 0px 0px; - margin: 0px 0px; - padding-left: 1em; - background-color: white; - font-family: sans-serif; - background-repeat: no-repeat; - background-size: 100%; -} - -#page { - display: block; - padding: 0px; - margin: 0px; -} - -#header { - min-height: 100px; - max-width: 760px; - margin: 0 auto; - padding-left: 80px; - padding-right: 80px; - padding-top: 30px; -} - -#header h1 { - padding: 0; - margin: 0; -} - -/* Menu */ -ul#menu { - padding: 0; - display: block; - margin: auto; -} - -ul#menu li, div.button { - display: inline-block; - background-color: white; - padding: 5px; - font-size: .70em; - text-transform: uppercase; - width: 30%; - text-align: center; - font-weight: 600; -} - -div.button { - margin-top:5px; - width: 40%; -} - -#button_block {margin-top:50px;} - -ul#menu a.hover li { - background-color: red; -} - -/* Contents */ - -#main, #main_home { - display: block; - padding: 80px; - padding-top: 60px; /* BCP */ - font-size: 100%; - line-height: 100%; - max-width: 760px; - background-color: #ffffff; - margin: 0 auto; -} - -#main_home { - background-color: rgba(255, 255, 255, 0.5); -} - -#index_content div.intro p { - font-size: 12px; -} - -#main h1 { - /* line-height: 80%; */ - line-height: normal; - padding-top: 3px; - padding-bottom: 4px; - /* Demitri: font-size: 22pt; */ - font-size: 200%; /* BCP */ -} - -/* allow for multi-line headers */ -#main a.idref:visited {color : #416DFF; text-decoration : none; } -#main a.idref:link {color : #416DFF; text-decoration : none; } -#main a.idref:hover {text-decoration : none; } -#main a.idref:active {text-decoration : none; } - -#main a.modref:visited {color : #416DFF; text-decoration : none; } -#main a.modref:link {color : #416DFF; text-decoration : none; } -#main a.modref:hover {text-decoration : none; } -#main a.modref:active {text-decoration : none; } - -#main .keyword { color : #697f2f } -#main { color: black } - -/* General section class - applies to all .section IDs */ -.section { - padding-top: 12px; - padding-bottom: 11px; - padding-left: 8px; - margin-top: 5px; - margin-bottom: 3px; - margin-top: 18px; - font-size : 125%; - color: #ffffff; -} - -/* Book title in header */ -.booktitleinheader { - color: #000000; - text-transform: uppercase; - font-weight: 300; - letter-spacing: 1px; - font-size: 125%; - margin-left: 0px; - margin-bottom: 22px; - } - -/* Chapter titles */ -.libtitle { - max-width: 860px; - text-transform: uppercase; - margin: 5px auto; - font-weight: 500; - padding-bottom: 2px; - font-size: 120%; - letter-spacing: 3px; - } - -.subtitle { - display: block; - padding-top: 10px; - font-size: 70%; - line-height: normal; -} - -h2.section { - color: #2a2c71; - background-color: transparent; - padding-left: 0px; - padding-top: 0px; - padding-bottom: 0px; - /* margin-top: 0px; */ - margin-top: 9px; /* BCP 2/20 */ - font-size : 135%; } - -h3.section { - /* background-color: rgb(90%,90%,100%); */ - background-color: white; - /* padding-left: 8px; */ - padding-left: 0px; - /* padding-top: 7px; */ - padding-top: 0px; - /* padding-bottom: 0px; */ - padding-bottom: 0.5em; - /* margin-top: 9px; */ - /* margin-top: 4px; (BCP 2/20) */ - margin-top: 9px; /* BCP 2/20 */ - font-size : 115%; - color:black; -} - -h4.section { - margin-top: .2em; - background-color: white; - color: #2a2c71; - padding-left: 0px; - padding-top: 0px; - padding-bottom: 0.5em; /* 0px; */ - font-size : 100%; - font-style : bold; - text-decoration : underline; -} - -#header p { - font-size: 13px; -} - -/* Sets up Main ID and margins */ - -#main .doc { - margin: 0px auto; - font-size: 14px; - line-height: 22px; - /* max-width: 570px; */ - color: black; - /* text-align: justify; */ - border-style: plain; - /* This might work better after changing back to standard coqdoc: */ - padding-top: 10px; - /* padding-top: 18px; */ -} - -.quote { - margin-left: auto; - margin-right: auto; - width: 40em; - color: darkred; -} - -.loud { - color: darkred; -} - -pre { - margin-top: 0px; - margin-bottom: 0px; -} - -.inlinecode { - display: inline; - /* font-size: 125%; */ - color: #444444; - font-family: monospace } - -.doc .inlinecode { - display: inline; - font-size: 105%; - color: rgb(35%,35%,70%); - font-family: monospace } - -.doc .inlinecode .id { -/* I am changing this to white in style below: - color: rgb(35%,35%,70%); -*/ -} - -h1 .inlinecode .id, h1.section span.inlinecode { - color: #ffffff; -} - -.inlinecodenm { - display: inline; - /* font-size: 125%; */ - color: #444444; -} - -.doc .inlinecodenm { - display: inline; - color: rgb(35%,35%,70%); -} - -.doc .inlinecodenm .id { - color: rgb(35%,35%,70%); -} - -.doc .code { - display: inline; - font-size: 110%; - color: rgb(35%,35%,70%); - font-family: monospace; - padding-left: 0px; -} - -.comment { - display: inline; - font-family: monospace; - color: rgb(50%,50%,80%); -} - -.inlineref { - display: inline; - /* font-family: monospace; */ - color: rgb(50%,50%,80%); -} - -.show::before { - /* content: "more"; */ - content: "+"; -} - -.show { - background-color: rgb(93%,93%,93%); - display: inline; - font-family: monospace; - font-size: 60%; - padding-top: 1px; - padding-bottom: 2px; - padding-left: 4px; - padding-right: 4px; - color: rgb(60%,60%,60%); -} - -/* -.show { - display: inline; - font-family: monospace; - font-size: 60%; - padding-top: 0px; - padding-bottom: 0px; - padding-left: 10px; - border: 1px; - border-style: solid; - color: rgb(75%,75%,85%); -} -*/ - -.proofbox { - font-size: 90%; - color: rgb(75%,75%,75%); -} - -#main .less-space { - margin-top: -12px; -} - -/* Inline quizzes */ -.quiz:before { - color: rgb(40%,40%,40%); - /* content: "- Quick Check -" ; */ - display: block; - text-align: center; - margin-bottom: 5px; -} -.quiz { - border: 4px; - border-color: rgb(80%,80%,80%); - /* - margin-left: 40px; - margin-right: 100px; - */ - padding: 5px; - padding-left: 8px; - padding-right: 8px; - margin-top: 10px; - margin-bottom: 15px; - border-style: solid; -} - -/* For textual ones... */ -.show-old { - display: inline; - font-family: monospace; - font-size: 80%; - padding-top: 0px; - padding-bottom: 0px; - padding-left: 3px; - padding-right: 3px; - border: 1px; - margin-top: 5px; /* doesn't work?! */ - border-style: solid; - color: rgb(75%,75%,85%); -} - -.largebr { - margin-top: 10px; -} - -.code { - padding-left: 20px; - font-size: 14px; - font-family: monospace; - line-height: 17px; - margin-top: 9px; -} - -/* Working: -.code { - display: block; - padding-left: 0px; - font-size: 110%; - font-family: monospace; - } -*/ - -.code-space { - max-width: 50em; - margin-top: 0em; - /* margin-bottom: -.5em; */ - margin-left: auto; - margin-right: auto; -} - -.code-tight { - max-width: 50em; - margin-top: .6em; - /* margin-bottom: -.7em; */ - margin-left: auto; - margin-right: auto; -} - -hr.doublespaceincode { - height: 1pt; - visibility: hidden; - font-size: 10px; -} - -/* -code.br { - height: 5em; -} -*/ - -#main .citation { - color: rgb(70%,0%,0%); - text-decoration: underline; -} - -table.infrule { - border: 0px; - margin-left: 50px; - margin-top: .5em; - margin-bottom: 1.2em; -} - -td.infrule { - font-family: monospace; - text-align: center; - /* color: rgb(35%,35%,70%); */ - padding: 0px; - line-height: 100%; -} - -tr.infrulemiddle hr { - margin: 1px 0 1px 0; -} - -.infrulenamecol { - color: rgb(60%,60%,60%); - font-size: 80%; - padding-left: 1em; - padding-bottom: 0.1em -} - -#footer { - font-size: 65%; - font-family: sans-serif; -} - -.id { display: inline; } - -.id[title="constructor"] { - color: #697f2f; -} - -.id[title="var"], -.id[title="variable"] { - color: rgb(40%,0%,40%); -} - -.id[title="definition"] { - color: rgb(0%,40%,0%); -} - -.id[title="abbreviation"] { - color: rgb(0%,40%,0%); -} - -.id[title="lemma"] { - color: rgb(0%,40%,0%); -} - -.id[title="instance"] { - color: rgb(0%,40%,0%); -} - -.id[title="projection"] { - color: rgb(0%,40%,0%); -} - -.id[title="method"] { - color: rgb(0%,40%,0%); -} - -.id[title="inductive"] { - color: #034764; -} - -.id[title="record"] { - color: rgb(0%,0%,80%); -} - -.id[title="class"] { - color: rgb(0%,0%,80%); -} - -.id[title="keyword"] { - color : #697f2f; - /* color: black; */ -} - -.inlinecode .id { - color: rgb(0%,0%,0%); -} - -.nowrap { - white-space: nowrap; -} - -.HIDEFROMHTML { - display: none; -} - -/* TOC */ - -#toc h2 { -/* padding-top: 13px; */ - padding-bottom: 13px; - padding-left: 8px; - margin-top: 5px; - margin-top: 20px; - /* OLD: padding: 10px; - line-height: 120%; - background-color: rgb(60%,60%,100%); */ -} - -#toc h2.ui-accordion-header { - padding: .5em .5em .5em .7em; - outline: none; -} - -#toc .ui-accordion .ui-accordion-content { - padding: 0.5em 2.5em 0.8em .9em; - border-top: 0; - margin-bottom: 1em; - /* bottom rule */ - border: none; - border-bottom: 1px solid transparent; - transition: border-bottom-color 0.25s ease-in; - transition-delay: 0.15s; -} - -#toc .ui-accordion .ui-accordion-content-active { - border-bottom: 1px solid #9b9b9b; - transition-delay: 0s; -} - -#toc h2.ui-accordion-header-active { - background: silver !important; -} - -#toc h2:not(.ui-accordion-header-active):hover { - background: rgba(0,0,0,0.04) !important; -} - -#toc h2 a:hover { - text-decoration: underline; -} - -#toc h2:hover::after { - content: "expand ▾"; - font-size: 80%; - float: right; - margin-top: 0.2em; - color: silver; - opacity: 1; - transition: opacity .5s ease-in-out; -} - -#toc h2.ui-accordion-header-active:hover::after { - opacity: 0; -} - -#toc h2 .select { background-image: url('media/image/arrow_down.jpg'); } -div#sec1.hide { display: none; } - -#toc ul { - padding-top: 8px; - font-size: 14px; - padding-left: 0; -} - -#toc ul ul { - margin-bottom: -8px; -} - -#toc li { - font-weight: 600; - list-style-type: none; - padding-top: 12px; - padding-bottom: 8px; -} - -#toc li li { - font-weight: 300; - list-style-type: circle; - padding-bottom: 3px; - padding-top: 0px; - margin-left: 19px; -} - - - - -/* Accordion Overrides */ - -/* Widget Bar */ -.ui-state-default, -.ui-widget-content .ui-state-default, -.ui-widget-header .ui-state-default, -.ui-button, -/* We use html here because we need a greater specificity to make sure disabled - works properly when clicked or hovered */ -html .ui-button.ui-state-disabled:hover, -html .ui-button.ui-state-disabled:active { - border: none!important; - /* BCP 3/17: I like it better without the rules... - border-bottom: 1px solid silver!important; */ - background: white !important; - font-weight: normal; - color: #454545!important; - font-weight: 400!important; - margin-top: 0px!important; - -} - -/* Misc visuals -----------------------------------*/ - -/* Corner radius */ -.ui-corner-all, -.ui-corner-top, -.ui-corner-left, -.ui-corner-tl { - border-top-left-radius: 0px!important; -} - -.ui-corner-all, -.ui-corner-top, -.ui-corner-right, -.ui-corner-tr { - border-top-right-radius: 0px!important; -} - -.ui-corner-all, -.ui-corner-bottom, -.ui-corner-left, -.ui-corner-bl { - border-bottom-left-radius: 0px!important; -} - -.ui-corner-all, -.ui-corner-bottom, -.ui-corner-right, -.ui-corner-br { - border-bottom-right-radius: 0px!important; -} - -html .ui-button.ui-state-disabled:focus { - color: red!important; -} - -/* Remove Icon */ -.ui-icon { display: none!important; } - -/* Widget */ -.ui-widget-content { - border: 1px solid #9e9e9e; - border-bottom-color: #b2b2b2; -} - -.ui-widget-content { - background: #ffffff; - color: #333333; -} - - -/* Index */ - -#index { - margin: 0; - padding: 0; - width: 100%; - font-style : normal; -} - -#index #frontispiece { - margin: auto; - padding: 1em; - width: 700px; -} - -.booktitle { - font-size : 300%; line-height: 100%; font-style:bold; - color: white; - padding-top: 70px; - padding-bottom: 20px; } -.authors { font-size : 200%; - line-height: 115%; } -.moreauthors { font-size : 170% } -.buttons { font-size : 170%; - margin-left: auto; - margin-right: auto; - font-style : bold; - } - -/* Link colors never changes */ - -A:link, A:visited, A:active, A:hover { - text-decoration: none; - color: #555555 -} - -/* Special color for the chapter header */ - -.booktitleinheader A:visited, .booktitleinheader A:active, .booktitleinheader A:hover, .booktitleinheader A:link { - text-decoration: none; - color: black; -} - -#index #entrance { - text-align: center; -} - -/* This was removed via CSS but the HTML is still generated */ -#index #footer { - display: none; -} - -.paragraph { - height: 0.6em; -} - -ul.doclist { - margin-top: 0em; - margin-bottom: 0em; -} - -/* Index styles */ - -/* Styles the author box (Intro class) and With (column class) */ - -.column { - float:left; - width: 43%; - margin:0 10px; - text-align: left; - font-size: 15px; - line-height: 25px; - padding-right: 20px; - min-height: 340px; -} - -.smallauthors { - font-size: 19px; - line-height: 25px; -} - -.mediumauthors { - font-size: 23px; - line-height: 33px; -} - -.largeauthors { - font-size: 28px; - line-height: 40px; -} - -.intro { - width: 35%; - font-size: 21px; - line-height: 27px; - font-weight: 600; - padding-right: 20px; -} - -.column.pub { - width: 40%; - margin-bottom: 20px; -} - -#index_content { - width: 100%!important; - display: block; - min-height: 400px; -} - -div.column.pub table tbody tr td { - text-align: center; padding: 10px; -} -div.column.pub table tbody tr td p { - text-align: left; - margin-top: 0; - font-weight: 600; - font-size: 13px!important; - line-height: 18px; -} - -/* Tables */ - -td.tab { - height: 16px; - font-weight: 600; - padding-left: 5px; - text-align: left!important; -} - -/* Styles tables on the index -- body class sf_home is used there */ - -body.sf_home table { - min-height: 450px; - vertical-align: top; -} - -body.sf_home table td { - vertical-align: top; - -} -body.sf_home table td p { - min-height: 100px; - -} - -table.logical { background-color: rgba(144, 160, 209, 0.5); } -table.logical tbody tr td.tab { background-color: #91a1d1; } - -table.language_found { background-color: rgba(178, 88, 88, 0.5); } -table.language_found tbody tr td.tab { background-color: #b25959; } - -table.algo { background-color: rgba(194, 194, 108, 0.5); } -table.algo tbody tr td.tab { background-color: #c2c26c; } - -table.qc { background-color: rgba(185, 170, 185, 0.5); } -table.qc tbody tr td.tab { background-color: #8b7d95; } - -table.vc { background-color: rgba(159, 125, 140, 0.5); } -table.vc tbody tr td.tab { background-color: rgb(159, 125, 140); } - -table.slf { background-color: rgba(219, 178, 127, 0.5); } -table.slf tbody tr td.tab { background-color: rgb(219, 178, 127); } - -/* Suggested background color for next volume */ -/* #c07d62 */ - -.ui-draggable, .ui-droppable { - background-position: top; -} - -/* Chapter dependencies (SVG) */ -.deps a polygon:hover { opacity: 0.6; stroke-width: 2; } -.deps a text { pointer-events: none; } - -/* A few specific things for the top-level SF landing page */ - -body.sf_home {background-color: #ededed; background-image: url(../media/image/core_mem_bg.jpg); } - -body.sf_home #header { - background-image: url(../media/image/core_mem_hdr_bg.jpg); - padding-bottom: 20px; -} - -body.sf_home #main_home { - background-color: transparent; -} - -/* A partial fix to a coqdoc bug... - See https://github.com/DeepSpec/sfdev/issues/236 */ -.inlinecode { white-space: pre; } -.inlinecode br { display: none; } - -#header { background-color: rgba(190, 170, 190, 0.5); } - -/* This volume's color */ -.section, ul#menu li.section_name, div.button { background-color: #8b7d95; } - -.slide img { - border: 2px solid gray; - margin: 1em; -} diff --git a/docs/res/fdl.org b/docs/res/fdl.org deleted file mode 100644 index 81e2cd9..0000000 --- a/docs/res/fdl.org +++ /dev/null @@ -1,489 +0,0 @@ -# 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/res/install-deps.el b/docs/res/install-deps.el deleted file mode 100644 index 09cf4ae..0000000 --- a/docs/res/install-deps.el +++ /dev/null @@ -1,11 +0,0 @@ -(require 'package) -(package-initialize) -(add-to-list 'package-archives '("nongnu" . "https://elpa.nongnu.org/nongnu/") t) -(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t) -(add-to-list 'package-archives '("gnu-devel" . "https://elpa.gnu.org/devel/") t) -(package-refresh-contents) - -(package-install 'org) -(package-install 'org-contrib) -(package-install 'org-transclusion) -(package-install 'htmlize) diff --git a/docs/res/publish.el b/docs/res/publish.el deleted file mode 100644 index c083eb0..0000000 --- a/docs/res/publish.el +++ /dev/null @@ -1,23 +0,0 @@ -(require 'package) -(package-initialize) - -(require 'org) -(require 'org-transclusion) -(require 'ox) -(require 'ox-html) -(require 'htmlize) -(require 'ox-texinfo) -(require 'ox-man) - -(setq org-transclusion-exclude-elements nil - org-html-head-include-default-style nil - org-html-head-include-scripts nil - org-html-postamble-format '(("en" "")) - org-html-postamble t - org-html-divs '((preamble "header" "header") - (content "article" "content") - (postamble "footer" "postamble")) - org-html-doctype "html5" - org-html-htmlize-output-type 'css) - -(org-transclusion-add-all) diff --git a/src/Compiler.v b/src/Compiler.v index cd05aa9..d6d87e2 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -1,22 +1,21 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * 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 . - *) - (*| +.. + Vericert: Verified high-level synthesis. + Copyright (C) 2019-2022 Yann Herklotz + + 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 . + ============== Compiler Proof ============== @@ -27,9 +26,12 @@ backwards simulation correct. Imports ======= + We first need to import all of the modules that are used in the correctness proof, which includes all of the passes that are performed in Vericert and the CompCert front end. + +.. coq:: none |*) Require compcert.backend.Selection. @@ -133,24 +135,28 @@ Definition partial_if {A: Type} Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. -Definition match_if {A: Type} (flag: unit -> bool) (R: A -> A -> Prop): A -> A -> Prop := +Definition match_if {A: Type} (flag: unit -> bool) (R: A -> A -> Prop) + : A -> A -> Prop := if flag tt then R else eq. Lemma total_if_match: - forall (A: Type) (flag: unit -> bool) (f: A -> A) (rel: A -> A -> Prop) (prog: A), - (forall p, rel p (f p)) -> + forall (A: Type) (flag: unit -> bool) (f: A -> A) + (rel: A -> A -> Prop) (prog: A), + (forall p, rel p (f p)) -> match_if flag rel prog (total_if flag f prog). Proof. intros. unfold match_if, total_if. destruct (flag tt); auto. Qed. Lemma partial_if_match: - forall (A: Type) (flag: unit -> bool) (f: A -> res A) (rel: A -> A -> Prop) (prog tprog: A), + forall (A: Type) (flag: unit -> bool) (f: A -> res A) + (rel: A -> A -> Prop) (prog tprog: A), (forall p tp, f p = OK tp -> rel p tp) -> partial_if flag f prog = OK tprog -> match_if flag rel prog tprog. Proof. - intros. unfold match_if, partial_if in *. destruct (flag tt). auto. congruence. + intros. unfold match_if, partial_if in *. destruct (flag tt). + auto. congruence. Qed. Remark forward_simulation_identity: @@ -164,12 +170,14 @@ Proof. Qed. Lemma match_if_simulation: - forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (transf: A -> A -> Prop) (prog tprog: A), + forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) + (transf: A -> A -> Prop) (prog tprog: A), match_if flag transf prog tprog -> (forall p tp, transf p tp -> forward_simulation (sem p) (sem tp)) -> forward_simulation (sem prog) (sem tprog). Proof. - intros. unfold match_if in *. destruct (flag tt). eauto. subst. apply forward_simulation_identity. + intros. unfold match_if in *. destruct (flag tt). eauto. subst. + apply forward_simulation_identity. Qed. (*| @@ -188,13 +196,16 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@ print (print_RTL 1) @@ Renumber.transf_program @@ print (print_RTL 2) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@ total_if Compopts.optim_constprop + (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 3) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop + (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 4) @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 5) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@@ partial_if Compopts.optim_redundancy + (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 6) @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 7) @@ -220,8 +231,10 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program := @@ print (print_RTL 0) @@@ transf_backend. -(* This is an unverified version of transf_hls with some experimental additions such as scheduling -that aren't completed yet. *) +(*| +This is an unverified version of transf_hls with some experimental additions +such as scheduling that aren't completed yet. +|*) Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := OK p @@@ SimplExpr.transl_program @@ -234,13 +247,16 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@ print (print_RTL 1) @@ Renumber.transf_program @@ print (print_RTL 2) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@ total_if Compopts.optim_constprop + (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 3) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop + (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 4) @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 5) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@@ partial_if Compopts.optim_redundancy + (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 6) @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 7) @@ -280,7 +296,8 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass Unusedglobproof.match_prog - ::: (@mkpass _ _ HTLgenproof.match_prog (HTLgenproof.TransfHTLLink HTLgen.transl_program)) + ::: (@mkpass _ _ HTLgenproof.match_prog + (HTLgenproof.TransfHTLLink HTLgen.transl_program)) (*::: mkpass (match_if HLSOpts.optim_ram Memorygen.match_prog)*) ::: mkpass Veriloggenproof.match_prog ::: pass_nil _. @@ -305,22 +322,36 @@ Theorem transf_hls_match: Proof. intros p tp T. unfold transf_hls, time in T. simpl in T. - destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. - destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. - destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. - destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. - destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. + destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; + simpl in T; try discriminate. + destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; + simpl in T; try discriminate. + destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; + simpl in T; try discriminate. + destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; + simpl in T; try discriminate. + destruct (Selection.sel_program p4) as [p5|e] eqn:P5; + simpl in T; try discriminate. + rewrite ! compose_print_identity in T. + destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; + simpl in T; try discriminate. + unfold transf_backend, time in T. simpl in T. rewrite ! compose_print_identity in T. - destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. - unfold transf_backend, time in T. simpl in T. rewrite ! compose_print_identity in T. - destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate. + destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; + simpl in T; try discriminate. set (p8 := Renumber.transf_program p7) in *. - set (p9 := total_if Compopts.optim_constprop Constprop.transf_program p8) in *. - set (p10 := total_if Compopts.optim_constprop Renumber.transf_program p9) in *. - destruct (partial_if Compopts.optim_CSE CSE.transf_program p10) as [p11|e] eqn:P11; simpl in T; try discriminate. - destruct (partial_if Compopts.optim_redundancy Deadcode.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. - destruct (Unusedglob.transform_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. - destruct (HTLgen.transl_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. + set (p9 := total_if Compopts.optim_constprop + Constprop.transf_program p8) in *. + set (p10 := total_if Compopts.optim_constprop + Renumber.transf_program p9) in *. + destruct (partial_if Compopts.optim_CSE CSE.transf_program p10) + as [p11|e] eqn:P11; simpl in T; try discriminate. + destruct (partial_if Compopts.optim_redundancy Deadcode.transf_program p11) + as [p12|e] eqn:P12; simpl in T; try discriminate. + destruct (Unusedglob.transform_program p12) as [p13|e] eqn:P13; + simpl in T; try discriminate. + destruct (HTLgen.transl_program p13) as [p14|e] eqn:P14; + simpl in T; try discriminate. (*set (p15 := total_if HLSOpts.optim_ram Memorygen.transf_program p14) in *.*) set (p15 := Veriloggen.transl_program p14) in *. unfold match_prog; simpl. @@ -332,13 +363,18 @@ Proof. exists p6; split. apply RTLgenproof.transf_program_match; auto. exists p7; split. apply Inliningproof.transf_program_match; auto. exists p8; split. apply Renumberproof.transf_program_match; auto. - exists p9; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p10; split. apply total_if_match. apply Renumberproof.transf_program_match. - exists p11; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. - exists p12; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. + exists p9; split. apply total_if_match. + apply Constpropproof.transf_program_match. + exists p10; split. apply total_if_match. + apply Renumberproof.transf_program_match. + exists p11; split. eapply partial_if_match; eauto. + apply CSEproof.transf_program_match. + exists p12; split. eapply partial_if_match; eauto. + apply Deadcodeproof.transf_program_match. exists p13; split. apply Unusedglobproof.transf_program_match; auto. exists p14; split. apply HTLgenproof.transf_program_match; auto. - (*exists p15; split. apply total_if_match. apply Memorygen.transf_program_match; auto.*) + (*exists p15; split. apply total_if_match. + apply Memorygen.transf_program_match; auto.*) exists p15; split. apply Veriloggenproof.transf_program_match; auto. inv T. reflexivity. Qed. @@ -347,7 +383,8 @@ Theorem cstrategy_semantic_preservation: forall p tp, match_prog p tp -> forward_simulation (Cstrategy.semantics p) (Verilog.semantics tp) - /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp). + /\ backward_simulation (atomic (Cstrategy.semantics p)) + (Verilog.semantics tp). Proof. intros p tp M. unfold match_prog, pass_match in M; simpl in M. Ltac DestructM := @@ -357,7 +394,8 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p15)). + assert (F: forward_simulation (Cstrategy.semantics p) + (Verilog.semantics p15)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -376,24 +414,30 @@ Ltac DestructM := eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. + eapply match_if_simulation. eassumption. + exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. + eapply match_if_simulation. eassumption. + exact Renumberproof.transf_program_correct. eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. + eapply match_if_simulation. eassumption. + exact CSEproof.transf_program_correct. eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. + eapply match_if_simulation. eassumption. + exact Deadcodeproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Unusedglobproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply HTLgenproof.transf_program_correct. eassumption. (*eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Memorygen.transf_program_correct; eassumption.*) + eapply match_if_simulation. eassumption. + exact Memorygen.transf_program_correct; eassumption.*) eapply Veriloggenproof.transf_program_correct; eassumption. } split. auto. apply forward_to_backward_simulation. - apply factor_forward_simulation. auto. eapply sd_traces. eapply Verilog.semantics_determinate. + apply factor_forward_simulation. auto. eapply sd_traces. + eapply Verilog.semantics_determinate. apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive. apply Verilog.semantics_determinate. Qed. @@ -451,11 +495,13 @@ Theorem separate_transf_c_program_correct: link_list c_units = Some c_program -> exists verilog_program, link_list verilog_units = Some verilog_program - /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program). + /\ backward_simulation (Csem.semantics c_program) + (Verilog.semantics verilog_program). Proof. intros. assert (nlist_forall2 match_prog c_units verilog_units). - { eapply nlist_forall2_imply. eauto. simpl; intros. apply transf_hls_match; auto. } + { eapply nlist_forall2_imply. eauto. simpl; intros. + apply transf_hls_match; auto. } assert (exists verilog_program, link_list verilog_units = Some verilog_program /\ match_prog c_program verilog_program). { eapply link_list_compose_passes; eauto. } diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index d23850a..d308366 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -1,20 +1,32 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2022 Yann Herklotz - * - * 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 . - *) +(*| +.. + Vericert: Verified high-level synthesis. + Copyright (C) 2019-2022 Yann Herklotz + + 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 . + +============= +RTLBlockInstr +============= + +These instructions are used for ``RTLBlock`` and ``RTLPar``, so that they have +consistent instructions, which greatly simplifies the proofs, as they will by +default have the same instruction syntax and semantics. The only changes are +therefore at the top-level of the instructions. + +.. coq:: none +|*) Require Import Coq.micromega.Lia. @@ -34,15 +46,6 @@ Require Import Vericertlib. Definition node := positive. (*| -============= -RTLBlockInstr -============= - -These instructions are used for ``RTLBlock`` and ``RTLPar``, so that they have -consistent instructions, which greatly simplifies the proofs, as they will by -default have the same instruction syntax and semantics. The only changes are -therefore at the top-level of the instructions. - Instruction Definition ====================== -- cgit