aboutsummaryrefslogtreecommitdiffstats
path: root/doc
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-03-26 21:08:23 +0000
committerYann Herklotz <git@yannherklotz.com>2022-03-26 21:08:23 +0000
commit11d6215f265d0dbcfd0048819a614f318a0775a4 (patch)
tree16b0450e4df7caaed57400d503044ca92f1f3c38 /doc
parenta5b8a41ef22618c69db62dfeb71d7f38bbba34e2 (diff)
downloadvericert-11d6215f265d0dbcfd0048819a614f318a0775a4.tar.gz
vericert-11d6215f265d0dbcfd0048819a614f318a0775a4.zip
Add sphinx documentation
Diffstat (limited to 'doc')
-rw-r--r--doc/Makefile24
-rw-r--r--doc/Makefile.extr39
-rw-r--r--doc/README.org7
-rw-r--r--doc/_static/css/custom.css11
-rw-r--r--doc/_static/images/toolflow.pdfbin0 -> 20490 bytes
-rw-r--r--doc/_static/images/toolflow.pngbin0 -> 26864 bytes
-rw-r--r--doc/_static/images/toolflow.svg1250
-rw-r--r--doc/common.org15
-rw-r--r--doc/conf.py85
-rw-r--r--doc/documentation.org562
-rw-r--r--doc/docutils.conf2
-rw-r--r--doc/index.rst26
-rw-r--r--doc/make.bat35
-rw-r--r--doc/man.org89
-rw-r--r--doc/res/coqdoc.css867
-rw-r--r--doc/res/fdl.org489
-rw-r--r--doc/res/install-deps.el11
-rw-r--r--doc/res/publish.el23
-rw-r--r--doc/vericert.rst530
19 files changed, 4065 insertions, 0 deletions
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
--- /dev/null
+++ b/doc/_static/images/toolflow.pdf
Binary files differ
diff --git a/doc/_static/images/toolflow.png b/doc/_static/images/toolflow.png
new file mode 100644
index 0000000..601d6be
--- /dev/null
+++ b/doc/_static/images/toolflow.png
Binary files 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 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ width="308.97266pt"
+ height="124.71875pt"
+ viewBox="0 0 308.97267 124.71875"
+ version="1.2"
+ id="svg466"
+ xmlns:xlink="http://www.w3.org/1999/xlink"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:svg="http://www.w3.org/2000/svg">
+ <defs
+ id="defs183">
+ <g
+ id="g172">
+ <symbol
+ overflow="visible"
+ id="glyph0-0">
+ <path
+ style="stroke:none"
+ d=""
+ id="path25" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-1">
+ <path
+ style="stroke:none"
+ d="M 6.625,-2.328125 C 6.625,-2.421875 6.625,-2.5 6.5,-2.5 6.390625,-2.5 6.390625,-2.4375 6.375,-2.328125 6.296875,-0.90625 5.234375,-0.09375 4.140625,-0.09375 c -0.609375,0 -2.5625,-0.328125 -2.5625,-3.3125 0,-2.96875 1.953125,-3.3125 2.5625,-3.3125 1.078125,0 1.96875,0.90625 2.171875,2.359375 C 6.328125,-4.21875 6.328125,-4.1875 6.46875,-4.1875 6.625,-4.1875 6.625,-4.21875 6.625,-4.421875 V -6.78125 c 0,-0.171875 0,-0.25 -0.109375,-0.25 -0.03125,0 -0.078125,0 -0.15625,0.125 l -0.5,0.734375 C 5.5,-6.53125 4.984375,-7.03125 4.03125,-7.03125 c -1.875,0 -3.46875,1.59375 -3.46875,3.625 0,2.0625 1.609375,3.625 3.46875,3.625 1.625,0 2.59375,-1.390625 2.59375,-2.546875 z m 0,0"
+ id="path28" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-2">
+ <path
+ style="stroke:none"
+ d="m 2.546875,0 v -0.3125 c -0.671875,0 -0.78125,0 -0.78125,-0.4375 V -6.921875 L 0.328125,-6.8125 V -6.5 c 0.703125,0 0.78125,0.0625 0.78125,0.5625 V -0.75 c 0,0.4375 -0.109375,0.4375 -0.78125,0.4375 V 0 L 1.4375,-0.03125 Z m 0,0"
+ id="path31" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-3">
+ <path
+ style="stroke:none"
+ d="m 2.46875,0 v -0.3125 c -0.671875,0 -0.703125,-0.046875 -0.703125,-0.4375 V -4.40625 L 0.375,-4.296875 v 0.3125 c 0.640625,0 0.734375,0.0625 0.734375,0.546875 V -0.75 c 0,0.4375 -0.109375,0.4375 -0.78125,0.4375 V 0 l 1.09375,-0.03125 C 1.78125,-0.03125 2.125,-0.015625 2.46875,0 Z m -0.5625,-6.015625 c 0,-0.28125 -0.21875,-0.53125 -0.515625,-0.53125 -0.34375,0 -0.546875,0.28125 -0.546875,0.53125 C 0.84375,-5.75 1.078125,-5.5 1.375,-5.5 c 0.34375,0 0.53125,-0.265625 0.53125,-0.515625 z m 0,0"
+ id="path34" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-4">
+ <path
+ style="stroke:none"
+ d="m 4.828125,-4.03125 c 0,-0.171875 -0.109375,-0.484375 -0.5,-0.484375 -0.203125,0 -0.640625,0.0625 -1.0625,0.46875 C 2.84375,-4.375 2.4375,-4.40625 2.21875,-4.40625 c -0.9375,0 -1.625,0.6875 -1.625,1.453125 0,0.4375 0.21875,0.8125 0.46875,1.03125 -0.125,0.140625 -0.3125,0.46875 -0.3125,0.828125 0,0.3125 0.140625,0.6875 0.453125,0.890625 -0.609375,0.15625 -0.921875,0.59375 -0.921875,0.984375 0,0.71875 0.984375,1.265625 2.203125,1.265625 1.171875,0 2.203125,-0.5 2.203125,-1.28125 0,-0.34375 -0.125,-0.859375 -0.640625,-1.140625 -0.53125,-0.265625 -1.109375,-0.265625 -1.71875,-0.265625 -0.25,0 -0.671875,0 -0.75,-0.015625 C 1.265625,-0.703125 1.0625,-1 1.0625,-1.328125 c 0,-0.03125 0,-0.265625 0.15625,-0.46875 0.390625,0.28125 0.8125,0.3125 1,0.3125 0.921875,0 1.609375,-0.6875 1.609375,-1.453125 0,-0.375 -0.15625,-0.734375 -0.40625,-0.96875 C 3.78125,-4.25 4.140625,-4.296875 4.3125,-4.296875 c 0,0 0.078125,0 0.109375,0.015625 C 4.3125,-4.25 4.25,-4.140625 4.25,-4.015625 c 0,0.171875 0.140625,0.28125 0.296875,0.28125 0.09375,0 0.28125,-0.0625 0.28125,-0.296875 z m -1.75,1.078125 c 0,0.265625 0,0.59375 -0.15625,0.84375 C 2.84375,-2 2.609375,-1.71875 2.21875,-1.71875 c -0.875,0 -0.875,-1 -0.875,-1.21875 0,-0.265625 0.015625,-0.59375 0.15625,-0.84375 0.078125,-0.109375 0.3125,-0.390625 0.71875,-0.390625 0.859375,0 0.859375,0.984375 0.859375,1.21875 z m 1.09375,3.734375 c 0,0.546875 -0.703125,1.046875 -1.671875,1.046875 -1.015625,0 -1.703125,-0.515625 -1.703125,-1.046875 0,-0.453125 0.375,-0.828125 0.8125,-0.84375 h 0.59375 c 0.859375,0 1.96875,0 1.96875,0.84375 z m 0,0"
+ id="path37" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-5">
+ <path
+ style="stroke:none"
+ d="m 5.328125,0 v -0.3125 c -0.515625,0 -0.765625,0 -0.765625,-0.296875 v -1.90625 c 0,-0.859375 0,-1.15625 -0.3125,-1.515625 -0.140625,-0.171875 -0.46875,-0.375 -1.046875,-0.375 -0.84375,0 -1.28125,0.59375 -1.4375,0.953125 H 1.75 v -3.46875 L 0.3125,-6.8125 V -6.5 c 0.703125,0 0.78125,0.0625 0.78125,0.5625 V -0.75 c 0,0.4375 -0.109375,0.4375 -0.78125,0.4375 V 0 L 1.453125,-0.03125 2.5625,0 v -0.3125 c -0.671875,0 -0.78125,0 -0.78125,-0.4375 V -2.59375 C 1.78125,-3.625 2.5,-4.1875 3.125,-4.1875 c 0.640625,0 0.75,0.53125 0.75,1.109375 V -0.75 c 0,0.4375 -0.109375,0.4375 -0.78125,0.4375 V 0 l 1.125,-0.03125 z m 0,0"
+ id="path40" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-6">
+ <path
+ style="stroke:none"
+ d="m 3.3125,-1.234375 v -0.5625 h -0.25 V -1.25 c 0,0.734375 -0.296875,1.109375 -0.671875,1.109375 -0.671875,0 -0.671875,-0.90625 -0.671875,-1.078125 v -2.765625 h 1.4375 v -0.3125 H 1.71875 V -6.125 h -0.25 c 0,0.8125 -0.296875,1.875 -1.28125,1.921875 v 0.21875 h 0.84375 v 2.75 c 0,1.21875 0.9375,1.34375 1.296875,1.34375 0.703125,0 0.984375,-0.703125 0.984375,-1.34375 z m 0,0"
+ id="path43" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-7">
+ <path
+ style="stroke:none"
+ d="m 8.109375,0 v -0.3125 c -0.515625,0 -0.765625,0 -0.78125,-0.296875 v -1.90625 c 0,-0.859375 0,-1.15625 -0.3125,-1.515625 -0.140625,-0.171875 -0.46875,-0.375 -1.046875,-0.375 -0.828125,0 -1.28125,0.59375 -1.4375,0.984375 C 4.390625,-4.296875 3.65625,-4.40625 3.203125,-4.40625 2.46875,-4.40625 2,-3.984375 1.71875,-3.359375 V -4.40625 L 0.3125,-4.296875 v 0.3125 c 0.703125,0 0.78125,0.0625 0.78125,0.5625 V -0.75 c 0,0.4375 -0.109375,0.4375 -0.78125,0.4375 V 0 L 1.453125,-0.03125 2.5625,0 v -0.3125 c -0.671875,0 -0.78125,0 -0.78125,-0.4375 V -2.59375 C 1.78125,-3.625 2.5,-4.1875 3.125,-4.1875 c 0.640625,0 0.75,0.53125 0.75,1.109375 V -0.75 c 0,0.4375 -0.109375,0.4375 -0.78125,0.4375 V 0 L 4.21875,-0.03125 5.328125,0 v -0.3125 c -0.65625,0 -0.765625,0 -0.765625,-0.4375 v -1.84375 c 0,-1.03125 0.703125,-1.59375 1.34375,-1.59375 0.625,0 0.734375,0.53125 0.734375,1.109375 V -0.75 c 0,0.4375 -0.109375,0.4375 -0.78125,0.4375 V 0 l 1.125,-0.03125 z m 0,0"
+ id="path46" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-8">
+ <path
+ style="stroke:none"
+ d="m 5.328125,0 v -0.3125 c -0.515625,0 -0.765625,0 -0.765625,-0.296875 v -1.90625 c 0,-0.859375 0,-1.15625 -0.3125,-1.515625 -0.140625,-0.171875 -0.46875,-0.375 -1.046875,-0.375 C 2.46875,-4.40625 2,-3.984375 1.71875,-3.359375 V -4.40625 L 0.3125,-4.296875 v 0.3125 c 0.703125,0 0.78125,0.0625 0.78125,0.5625 V -0.75 c 0,0.4375 -0.109375,0.4375 -0.78125,0.4375 V 0 L 1.453125,-0.03125 2.5625,0 v -0.3125 c -0.671875,0 -0.78125,0 -0.78125,-0.4375 V -2.59375 C 1.78125,-3.625 2.5,-4.1875 3.125,-4.1875 c 0.640625,0 0.75,0.53125 0.75,1.109375 V -0.75 c 0,0.4375 -0.109375,0.4375 -0.78125,0.4375 V 0 l 1.125,-0.03125 z m 0,0"
+ id="path49" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-9">
+ <path
+ style="stroke:none"
+ d="M 4.6875,-2.140625 C 4.6875,-3.40625 3.703125,-4.46875 2.5,-4.46875 c -1.25,0 -2.21875,1.09375 -2.21875,2.328125 0,1.296875 1.03125,2.25 2.203125,2.25 1.203125,0 2.203125,-0.984375 2.203125,-2.25 z M 3.875,-2.21875 c 0,0.359375 0,0.90625 -0.21875,1.34375 -0.234375,0.453125 -0.671875,0.734375 -1.15625,0.734375 -0.4375,0 -0.875,-0.203125 -1.140625,-0.671875 -0.25,-0.4375 -0.25,-1.046875 -0.25,-1.40625 0,-0.390625 0,-0.921875 0.234375,-1.359375 C 1.609375,-4.03125 2.078125,-4.25 2.484375,-4.25 c 0.4375,0 0.859375,0.21875 1.125,0.65625 0.265625,0.421875 0.265625,1 0.265625,1.375 z m 0,0"
+ id="path52" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-10">
+ <path
+ style="stroke:none"
+ d="m 3.625,-3.796875 c 0,-0.3125 -0.3125,-0.609375 -0.734375,-0.609375 -0.734375,0 -1.09375,0.671875 -1.21875,1.09375 V -4.40625 L 0.28125,-4.296875 v 0.3125 c 0.703125,0 0.78125,0.0625 0.78125,0.5625 V -0.75 c 0,0.4375 -0.109375,0.4375 -0.78125,0.4375 V 0 l 1.140625,-0.03125 c 0.390625,0 0.859375,0 1.265625,0.03125 V -0.3125 H 2.46875 c -0.734375,0 -0.75,-0.109375 -0.75,-0.46875 V -2.3125 c 0,-0.984375 0.421875,-1.875 1.171875,-1.875 0.0625,0 0.09375,0 0.109375,0.015625 -0.03125,0 -0.234375,0.125 -0.234375,0.390625 0,0.265625 0.21875,0.421875 0.4375,0.421875 0.171875,0 0.421875,-0.125 0.421875,-0.4375 z m 0,0"
+ id="path55" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-11">
+ <path
+ style="stroke:none"
+ d="m 4.96875,-1.859375 c 0,-0.984375 -0.65625,-1.8125 -1.484375,-2.015625 l -1.28125,-0.296875 c -0.625,-0.15625 -1,-0.6875 -1,-1.265625 0,-0.703125 0.53125,-1.3125 1.3125,-1.3125 1.65625,0 1.875,1.640625 1.9375,2.078125 0.015625,0.0625 0.015625,0.125 0.125,0.125 0.125,0 0.125,-0.046875 0.125,-0.234375 v -2 c 0,-0.171875 0,-0.25 -0.109375,-0.25 -0.0625,0 -0.078125,0.015625 -0.140625,0.140625 l -0.359375,0.5625 C 3.796875,-6.625 3.390625,-7.03125 2.5,-7.03125 c -1.109375,0 -1.9375,0.875 -1.9375,1.9375 0,0.828125 0.53125,1.5625 1.296875,1.828125 0.109375,0.03125 0.625,0.15625 1.328125,0.328125 0.265625,0.0625 0.5625,0.140625 0.84375,0.5 0.203125,0.265625 0.3125,0.59375 0.3125,0.921875 0,0.703125 -0.5,1.421875 -1.34375,1.421875 -0.28125,0 -1.046875,-0.046875 -1.578125,-0.53125 C 0.84375,-1.171875 0.8125,-1.796875 0.8125,-2.15625 0.796875,-2.265625 0.71875,-2.265625 0.6875,-2.265625 c -0.125,0 -0.125,0.078125 -0.125,0.25 v 2 c 0,0.171875 0,0.234375 0.109375,0.234375 0.0625,0 0.078125,-0.015625 0.140625,-0.125 0,0 0.03125,-0.046875 0.359375,-0.578125 0.3125,0.34375 0.953125,0.703125 1.84375,0.703125 1.15625,0 1.953125,-0.96875 1.953125,-2.078125 z m 0,0"
+ id="path58" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-12">
+ <path
+ style="stroke:none"
+ d="m 4.140625,-1.1875 c 0,-0.09375 -0.078125,-0.125 -0.140625,-0.125 -0.078125,0 -0.109375,0.0625 -0.125,0.140625 -0.34375,1.03125 -1.25,1.03125 -1.34375,1.03125 -0.5,0 -0.890625,-0.296875 -1.125,-0.671875 -0.296875,-0.46875 -0.296875,-1.125 -0.296875,-1.484375 h 2.78125 c 0.21875,0 0.25,0 0.25,-0.21875 0,-0.984375 -0.546875,-1.953125 -1.78125,-1.953125 -1.15625,0 -2.078125,1.03125 -2.078125,2.28125 0,1.328125 1.046875,2.296875 2.1875,2.296875 C 3.6875,0.109375 4.140625,-1 4.140625,-1.1875 Z m -0.65625,-1.328125 h -2.375 C 1.171875,-4 2.015625,-4.25 2.359375,-4.25 c 1.015625,0 1.125,1.34375 1.125,1.734375 z m 0,0"
+ id="path61" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-13">
+ <path
+ style="stroke:none"
+ d="m 4.5625,-1.703125 c 0,-0.8125 -0.640625,-1.59375 -1.671875,-1.8125 0.8125,-0.265625 1.390625,-0.953125 1.390625,-1.75 0,-0.8125 -0.875,-1.375 -1.828125,-1.375 -1,0 -1.765625,0.59375 -1.765625,1.359375 0,0.328125 0.21875,0.515625 0.515625,0.515625 0.296875,0 0.5,-0.21875 0.5,-0.515625 0,-0.484375 -0.46875,-0.484375 -0.609375,-0.484375 0.296875,-0.5 0.953125,-0.625 1.3125,-0.625 0.421875,0 0.96875,0.21875 0.96875,1.109375 0,0.125 -0.03125,0.703125 -0.28125,1.140625 C 2.796875,-3.65625 2.453125,-3.625 2.203125,-3.625 2.125,-3.609375 1.890625,-3.59375 1.8125,-3.59375 c -0.078125,0.015625 -0.140625,0.03125 -0.140625,0.125 0,0.109375 0.0625,0.109375 0.234375,0.109375 h 0.4375 c 0.8125,0 1.1875,0.671875 1.1875,1.65625 0,1.359375 -0.6875,1.640625 -1.125,1.640625 -0.4375,0 -1.1875,-0.171875 -1.53125,-0.75 0.34375,0.046875 0.65625,-0.171875 0.65625,-0.546875 0,-0.359375 -0.265625,-0.5625 -0.546875,-0.5625 -0.25,0 -0.5625,0.140625 -0.5625,0.578125 0,0.90625 0.921875,1.5625 2.015625,1.5625 1.21875,0 2.125,-0.90625 2.125,-1.921875 z m 0,0"
+ id="path64" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-14">
+ <path
+ style="stroke:none"
+ d="M 7.140625,0 V -0.3125 H 6.96875 C 6.375,-0.3125 6.234375,-0.375 6.125,-0.703125 L 3.96875,-6.9375 c -0.046875,-0.125 -0.078125,-0.203125 -0.234375,-0.203125 -0.15625,0 -0.1875,0.0625 -0.234375,0.203125 L 1.4375,-0.984375 C 1.25,-0.46875 0.859375,-0.3125 0.3125,-0.3125 V 0 L 1.328125,-0.03125 2.484375,0 v -0.3125 c -0.5,0 -0.75,-0.25 -0.75,-0.5 0,-0.03125 0.015625,-0.140625 0.015625,-0.15625 L 2.21875,-2.265625 H 4.671875 L 5.203125,-0.75 c 0.015625,0.046875 0.03125,0.109375 0.03125,0.140625 0,0.296875 -0.5625,0.296875 -0.828125,0.296875 V 0 c 0.359375,-0.03125 1.0625,-0.03125 1.4375,-0.03125 z M 4.5625,-2.578125 H 2.328125 l 1.109375,-3.25 z m 0,0"
+ id="path67" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-15">
+ <path
+ style="stroke:none"
+ d="m 5.796875,-2.578125 h -0.25 c -0.109375,1.015625 -0.25,2.265625 -2,2.265625 h -0.8125 C 2.265625,-0.3125 2.25,-0.375 2.25,-0.703125 v -5.3125 C 2.25,-6.359375 2.25,-6.5 3.1875,-6.5 H 3.515625 V -6.8125 C 3.15625,-6.78125 2.25,-6.78125 1.84375,-6.78125 c -0.390625,0 -1.171875,0 -1.515625,-0.03125 V -6.5 H 0.5625 c 0.765625,0 0.796875,0.109375 0.796875,0.46875 v 5.25 c 0,0.359375 -0.03125,0.46875 -0.796875,0.46875 H 0.328125 V 0 h 5.1875 z m 0,0"
+ id="path70" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-16">
+ <path
+ style="stroke:none"
+ d="m 6.828125,-4.5 -0.1875,-2.25 h -6.09375 l -0.1875,2.25 h 0.25 C 0.75,-6.109375 0.890625,-6.4375 2.40625,-6.4375 c 0.171875,0 0.4375,0 0.53125,0.015625 0.21875,0.046875 0.21875,0.15625 0.21875,0.375 v 5.265625 c 0,0.328125 0,0.46875 -1.046875,0.46875 H 1.703125 V 0 C 2.109375,-0.03125 3.125,-0.03125 3.59375,-0.03125 c 0.453125,0 1.484375,0 1.890625,0.03125 v -0.3125 h -0.40625 c -1.046875,0 -1.046875,-0.140625 -1.046875,-0.46875 v -5.265625 c 0,-0.1875 0,-0.328125 0.1875,-0.375 0.109375,-0.015625 0.375,-0.015625 0.5625,-0.015625 1.515625,0 1.65625,0.328125 1.796875,1.9375 z m 0,0"
+ id="path73" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-17">
+ <path
+ style="stroke:none"
+ d="m 4.8125,-0.890625 v -0.5625 h -0.25 v 0.5625 C 4.5625,-0.3125 4.3125,-0.25 4.203125,-0.25 3.875,-0.25 3.84375,-0.703125 3.84375,-0.75 v -1.984375 c 0,-0.421875 0,-0.8125 -0.359375,-1.1875 C 3.09375,-4.3125 2.59375,-4.46875 2.109375,-4.46875 c -0.8125,0 -1.5,0.46875 -1.5,1.125 0,0.296875 0.203125,0.46875 0.453125,0.46875 0.28125,0 0.46875,-0.203125 0.46875,-0.453125 0,-0.125 -0.0625,-0.453125 -0.515625,-0.453125 C 1.28125,-4.140625 1.78125,-4.25 2.09375,-4.25 c 0.484375,0 1.0625,0.390625 1.0625,1.28125 v 0.359375 C 2.640625,-2.578125 1.9375,-2.546875 1.3125,-2.25 c -0.75,0.34375 -1,0.859375 -1,1.296875 0,0.8125 0.96875,1.0625 1.59375,1.0625 0.671875,0 1.125,-0.40625 1.3125,-0.859375 0.046875,0.390625 0.3125,0.8125 0.78125,0.8125 0.203125,0 0.8125,-0.140625 0.8125,-0.953125 z m -1.65625,-0.5 c 0,0.9375 -0.71875,1.28125 -1.171875,1.28125 -0.484375,0 -0.890625,-0.34375 -0.890625,-0.84375 0,-0.546875 0.40625,-1.375 2.0625,-1.4375 z m 0,0"
+ id="path76" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-18">
+ <path
+ style="stroke:none"
+ d="M 4.140625,-1.1875 C 4.140625,-1.28125 4.03125,-1.28125 4,-1.28125 c -0.078125,0 -0.109375,0.03125 -0.125,0.09375 -0.28125,0.921875 -0.9375,1.046875 -1.296875,1.046875 -0.53125,0 -1.40625,-0.421875 -1.40625,-2.03125 0,-1.625 0.8125,-2.046875 1.34375,-2.046875 0.09375,0 0.71875,0.015625 1.0625,0.375 -0.40625,0.03125 -0.46875,0.328125 -0.46875,0.453125 0,0.265625 0.1875,0.453125 0.453125,0.453125 0.265625,0 0.46875,-0.15625 0.46875,-0.46875 0,-0.671875 -0.765625,-1.0625 -1.53125,-1.0625 -1.25,0 -2.15625,1.078125 -2.15625,2.3125 0,1.28125 0.984375,2.265625 2.140625,2.265625 1.328125,0 1.65625,-1.203125 1.65625,-1.296875 z m 0,0"
+ id="path79" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-19">
+ <path
+ style="stroke:none"
+ d="m 4.5625,-2.03125 c 0,-1.265625 -0.890625,-2.21875 -2,-2.21875 -0.671875,0 -1.046875,0.5 -1.25,0.984375 v -0.25 c 0,-2.515625 1.234375,-2.875 1.75,-2.875 0.234375,0 0.65625,0.0625 0.875,0.40625 -0.15625,0 -0.546875,0 -0.546875,0.4375 0,0.3125 0.234375,0.46875 0.453125,0.46875 0.15625,0 0.46875,-0.09375 0.46875,-0.484375 0,-0.59375 -0.4375,-1.078125 -1.265625,-1.078125 -1.28125,0 -2.625,1.28125 -2.625,3.484375 0,2.671875 1.15625,3.375 2.078125,3.375 1.109375,0 2.0625,-0.9375 2.0625,-2.25 z M 3.65625,-2.046875 c 0,0.484375 0,0.984375 -0.171875,1.34375 C 3.1875,-0.109375 2.734375,-0.0625 2.5,-0.0625 c -0.625,0 -0.921875,-0.59375 -0.984375,-0.75 -0.1875,-0.46875 -0.1875,-1.265625 -0.1875,-1.4375 0,-0.78125 0.328125,-1.78125 1.21875,-1.78125 0.171875,0 0.625,0 0.9375,0.625 0.171875,0.359375 0.171875,0.875 0.171875,1.359375 z m 0,0"
+ id="path82" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-20">
+ <path
+ style="stroke:none"
+ d="m 4.6875,-1.640625 v -0.3125 H 3.703125 v -4.53125 c 0,-0.203125 0,-0.265625 -0.171875,-0.265625 -0.078125,0 -0.109375,0 -0.1875,0.125 l -3.0625,4.671875 v 0.3125 H 2.9375 v 0.859375 c 0,0.359375 -0.03125,0.46875 -0.765625,0.46875 H 1.96875 V 0 C 2.375,-0.03125 2.890625,-0.03125 3.3125,-0.03125 c 0.421875,0 0.9375,0 1.359375,0.03125 v -0.3125 h -0.21875 c -0.734375,0 -0.75,-0.109375 -0.75,-0.46875 v -0.859375 z m -1.703125,-0.3125 H 0.5625 l 2.421875,-3.71875 z m 0,0"
+ id="path85" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-21">
+ <path
+ style="stroke:none"
+ d="m 5.140625,0 v -0.3125 c -0.53125,0 -0.71875,-0.015625 -0.9375,-0.3125 L 2.859375,-2.34375 C 3.15625,-2.71875 3.53125,-3.203125 3.78125,-3.46875 4.09375,-3.828125 4.5,-3.984375 4.96875,-3.984375 v -0.3125 c -0.265625,0.015625 -0.5625,0.03125 -0.828125,0.03125 -0.296875,0 -0.828125,-0.015625 -0.953125,-0.03125 v 0.3125 c 0.21875,0.015625 0.296875,0.140625 0.296875,0.3125 0,0.15625 -0.109375,0.28125 -0.15625,0.34375 L 2.71875,-2.546875 1.9375,-3.5625 C 1.84375,-3.65625 1.84375,-3.671875 1.84375,-3.734375 c 0,-0.15625 0.15625,-0.25 0.34375,-0.25 v -0.3125 l -1.078125,0.03125 c -0.203125,0 -0.671875,-0.015625 -0.9375,-0.03125 v 0.3125 c 0.703125,0 0.703125,0 1.171875,0.609375 l 0.984375,1.28125 c -0.46875,0.59375 -0.46875,0.625 -0.9375,1.1875 C 0.921875,-0.328125 0.328125,-0.3125 0.125,-0.3125 V 0 c 0.25,-0.015625 0.5625,-0.03125 0.828125,-0.03125 L 1.890625,0 v -0.3125 c -0.21875,-0.03125 -0.28125,-0.15625 -0.28125,-0.3125 0,-0.21875 0.28125,-0.546875 0.890625,-1.265625 l 0.765625,1 C 3.34375,-0.78125 3.46875,-0.625 3.46875,-0.5625 c 0,0.09375 -0.09375,0.25 -0.359375,0.25 V 0 L 4.1875,-0.03125 c 0.265625,0 0.65625,0.015625 0.953125,0.03125 z m 0,0"
+ id="path88" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-22">
+ <path
+ style="stroke:none"
+ d="m 4.5625,-1.671875 c 0,-0.359375 -0.109375,-0.8125 -0.5,-1.234375 C 3.875,-3.109375 3.71875,-3.203125 3.078125,-3.609375 3.796875,-3.984375 4.28125,-4.5 4.28125,-5.15625 c 0,-0.921875 -0.875,-1.484375 -1.78125,-1.484375 -1,0 -1.8125,0.734375 -1.8125,1.671875 0,0.171875 0.015625,0.625 0.4375,1.09375 0.109375,0.109375 0.484375,0.359375 0.734375,0.53125 C 1.28125,-3.046875 0.421875,-2.5 0.421875,-1.5 c 0,1.046875 1.015625,1.71875 2.0625,1.71875 1.125,0 2.078125,-0.828125 2.078125,-1.890625 z M 3.84375,-5.15625 c 0,0.578125 -0.390625,1.046875 -0.984375,1.390625 L 1.625,-4.5625 c -0.453125,-0.296875 -0.5,-0.625 -0.5,-0.796875 0,-0.609375 0.65625,-1.03125 1.359375,-1.03125 0.71875,0 1.359375,0.515625 1.359375,1.234375 z M 4.0625,-1.3125 c 0,0.734375 -0.75,1.25 -1.5625,1.25 -0.859375,0 -1.578125,-0.609375 -1.578125,-1.4375 0,-0.578125 0.3125,-1.21875 1.15625,-1.6875 L 3.3125,-2.40625 c 0.28125,0.1875 0.75,0.484375 0.75,1.09375 z m 0,0"
+ id="path91" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-23">
+ <path
+ style="stroke:none"
+ d="m 7.140625,0 v -0.3125 h -0.25 c -0.765625,0 -0.78125,-0.109375 -0.78125,-0.46875 v -5.25 C 6.109375,-6.390625 6.125,-6.5 6.890625,-6.5 h 0.25 v -0.3125 c -0.359375,0.03125 -1.09375,0.03125 -1.46875,0.03125 -0.375,0 -1.125,0 -1.46875,-0.03125 V -6.5 H 4.4375 c 0.765625,0 0.78125,0.109375 0.78125,0.46875 v 2.328125 H 2.25 V -6.03125 C 2.25,-6.390625 2.265625,-6.5 3.03125,-6.5 h 0.234375 v -0.3125 c -0.34375,0.03125 -1.078125,0.03125 -1.46875,0.03125 -0.375,0 -1.125,0 -1.46875,-0.03125 V -6.5 H 0.5625 c 0.765625,0 0.796875,0.109375 0.796875,0.46875 v 5.25 c 0,0.359375 -0.03125,0.46875 -0.796875,0.46875 H 0.328125 V 0 c 0.34375,-0.03125 1.09375,-0.03125 1.46875,-0.03125 0.375,0 1.125,0 1.46875,0.03125 V -0.3125 H 3.03125 C 2.265625,-0.3125 2.25,-0.421875 2.25,-0.78125 v -2.609375 h 2.96875 v 2.609375 c 0,0.359375 -0.015625,0.46875 -0.78125,0.46875 H 4.203125 V 0 c 0.34375,-0.03125 1.078125,-0.03125 1.453125,-0.03125 0.390625,0 1.125,0 1.484375,0.03125 z m 0,0"
+ id="path94" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph0-24">
+ <path
+ style="stroke:none"
+ d="M 7.28125,-6.5 V -6.8125 C 6.96875,-6.78125 6.5625,-6.78125 6.3125,-6.78125 L 5.171875,-6.8125 V -6.5 C 5.6875,-6.484375 5.90625,-6.234375 5.90625,-6 c 0,0.078125 -0.03125,0.140625 -0.046875,0.203125 L 4.03125,-1 2.125,-6.03125 C 2.0625,-6.171875 2.0625,-6.203125 2.0625,-6.203125 2.0625,-6.5 2.625,-6.5 2.875,-6.5 V -6.8125 C 2.515625,-6.78125 1.828125,-6.78125 1.453125,-6.78125 L 0.1875,-6.8125 V -6.5 c 0.65625,0 0.84375,0 0.984375,0.375 L 3.484375,0 c 0.0625,0.1875 0.109375,0.21875 0.25,0.21875 0.15625,0 0.1875,-0.046875 0.234375,-0.1875 L 6.1875,-5.828125 C 6.328125,-6.203125 6.59375,-6.484375 7.28125,-6.5 Z m 0,0"
+ id="path97" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph1-0">
+ <path
+ style="stroke:none"
+ d=""
+ id="path100" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph1-1">
+ <path
+ style="stroke:none"
+ d="m 1.90625,-2.5 c 0,-0.28125 -0.234375,-0.515625 -0.515625,-0.515625 -0.296875,0 -0.53125,0.234375 -0.53125,0.515625 0,0.296875 0.234375,0.53125 0.53125,0.53125 0.28125,0 0.515625,-0.234375 0.515625,-0.53125 z m 0,0"
+ id="path103" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph2-0">
+ <path
+ style="stroke:none"
+ d=""
+ id="path106" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph2-1">
+ <path
+ style="stroke:none"
+ d="m 7.640625,-2.265625 c 0,-0.203125 -0.078125,-0.203125 -0.25,-0.203125 -0.125,0 -0.21875,0 -0.21875,0.171875 -0.078125,1.328125 -1.28125,1.9375 -2.28125,1.9375 -0.78125,0 -1.625,-0.234375 -2.140625,-0.84375 -0.46875,-0.578125 -0.59375,-1.3125 -0.59375,-2.21875 0,-0.5625 0.03125,-1.625 0.671875,-2.296875 0.640625,-0.65625 1.515625,-0.765625 2.03125,-0.765625 1.078125,0 2.015625,0.765625 2.234375,2.03125 C 7.125,-4.265625 7.140625,-4.25 7.359375,-4.25 c 0.265625,0 0.28125,-0.015625 0.28125,-0.28125 v -2.140625 c 0,-0.1875 0,-0.28125 -0.1875,-0.28125 -0.09375,0 -0.109375,0.03125 -0.1875,0.09375 l -0.65625,0.59375 c -0.625,-0.5 -1.28125,-0.6875 -1.96875,-0.6875 -2.484375,0 -4,1.484375 -4,3.53125 0,2.046875 1.515625,3.53125 4,3.53125 1.875,0 3,-1.21875 3,-2.375 z m 0,0"
+ id="path109" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph2-2">
+ <path
+ style="stroke:none"
+ d="m 5.40625,-2.171875 c 0,-1.34375 -0.921875,-2.34375 -2.546875,-2.34375 -1.640625,0 -2.546875,1.015625 -2.546875,2.34375 0,1.234375 0.890625,2.234375 2.546875,2.234375 1.671875,0 2.546875,-1.015625 2.546875,-2.234375 z M 4.125,-2.28125 c 0,0.859375 0,1.9375 -1.265625,1.9375 -1.265625,0 -1.265625,-1.078125 -1.265625,-1.9375 0,-0.453125 0,-0.953125 0.171875,-1.296875 0.1875,-0.375 0.609375,-0.578125 1.09375,-0.578125 0.421875,0 0.84375,0.15625 1.0625,0.5 C 4.125,-3.3125 4.125,-2.765625 4.125,-2.28125 Z m 0,0"
+ id="path112" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph2-3">
+ <path
+ style="stroke:none"
+ d="m 9.328125,0 v -0.46875 h -0.6875 v -2.578125 c 0,-1.03125 -0.515625,-1.4375 -1.546875,-1.4375 -0.90625,0 -1.421875,0.5 -1.6875,0.953125 -0.1875,-0.921875 -1.109375,-0.953125 -1.484375,-0.953125 -0.875,0 -1.4375,0.453125 -1.765625,1.078125 V -4.484375 L 0.453125,-4.40625 v 0.46875 c 0.609375,0 0.6875,0 0.6875,0.390625 v 3.078125 h -0.6875 V 0 l 1.25,-0.03125 1.25,0.03125 v -0.46875 h -0.6875 v -2.078125 c 0,-1.09375 0.875,-1.578125 1.5,-1.578125 0.328125,0 0.546875,0.203125 0.546875,0.96875 v 2.6875 H 3.625 V 0 L 4.890625,-0.03125 6.140625,0 v -0.46875 h -0.6875 V -2.546875 C 5.453125,-3.640625 6.3125,-4.125 6.9375,-4.125 7.28125,-4.125 7.5,-3.921875 7.5,-3.15625 v 2.6875 H 6.8125 V 0 l 1.25,-0.03125 z m 0,0"
+ id="path115" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph2-4">
+ <path
+ style="stroke:none"
+ d="m 5.984375,-2.21875 c 0,-1.328125 -0.90625,-2.265625 -2.34375,-2.265625 -0.75,0 -1.28125,0.3125 -1.5,0.484375 V -4.484375 L 0.375,-4.40625 v 0.46875 c 0.609375,0 0.6875,0 0.6875,0.375 V 1.46875 H 0.375 V 1.9375 L 1.625,1.90625 2.875,1.9375 V 1.46875 H 2.1875 v -1.859375 c 0.4375,0.34375 0.875,0.453125 1.28125,0.453125 1.5,0 2.515625,-0.90625 2.515625,-2.28125 z m -1.28125,0 c 0,1.40625 -0.703125,1.921875 -1.34375,1.921875 -0.140625,0 -0.609375,0 -1.0625,-0.546875 C 2.1875,-0.96875 2.1875,-0.984375 2.1875,-1.171875 V -3.28125 c 0,-0.1875 0.015625,-0.203125 0.15625,-0.34375 0.390625,-0.40625 0.921875,-0.46875 1.140625,-0.46875 0.65625,0 1.21875,0.609375 1.21875,1.875 z m 0,0"
+ id="path118" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph2-5">
+ <path
+ style="stroke:none"
+ d="m 4.921875,-1.171875 c 0,-0.171875 -0.1875,-0.171875 -0.234375,-0.171875 -0.171875,0 -0.1875,0.046875 -0.25,0.203125 -0.203125,0.484375 -0.78125,0.796875 -1.421875,0.796875 -1.40625,0 -1.421875,-1.328125 -1.421875,-1.828125 h 3.015625 c 0.21875,0 0.3125,0 0.3125,-0.265625 0,-0.3125 -0.0625,-1.046875 -0.5625,-1.546875 C 4,-4.34375 3.46875,-4.515625 2.78125,-4.515625 c -1.59375,0 -2.46875,1.03125 -2.46875,2.265625 0,1.34375 1,2.3125 2.609375,2.3125 1.578125,0 2,-1.0625 2,-1.234375 z M 3.984375,-2.5 H 1.59375 C 1.609375,-2.890625 1.625,-3.3125 1.828125,-3.640625 2.09375,-4.03125 2.5,-4.15625 2.78125,-4.15625 c 1.171875,0 1.1875,1.3125 1.203125,1.65625 z m 0,0"
+ id="path121" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph2-6">
+ <path
+ style="stroke:none"
+ d="m 4.40625,-3.671875 c 0,-0.53125 -0.53125,-0.8125 -1.0625,-0.8125 -0.6875,0 -1.09375,0.5 -1.3125,1.125 v -1.125 L 0.375,-4.40625 v 0.46875 c 0.609375,0 0.6875,0 0.6875,0.390625 V -0.46875 H 0.375 V 0 l 1.25,-0.03125 C 2,-0.03125 2.640625,-0.03125 3,0 V -0.46875 H 2.140625 v -1.75 c 0,-0.6875 0.234375,-1.90625 1.234375,-1.90625 0,0 -0.1875,0.171875 -0.1875,0.453125 0,0.40625 0.328125,0.609375 0.609375,0.609375 0.296875,0 0.609375,-0.203125 0.609375,-0.609375 z m 0,0"
+ id="path124" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph2-7">
+ <path
+ style="stroke:none"
+ d="m 3.8125,-1.234375 v -0.53125 H 3.34375 V -1.25 c 0,0.671875 -0.328125,0.90625 -0.609375,0.90625 -0.578125,0 -0.578125,-0.640625 -0.578125,-0.859375 v -2.75 H 3.625 v -0.46875 H 2.15625 v -1.90625 H 1.6875 c 0,1 -0.484375,1.984375 -1.484375,2.015625 v 0.359375 H 1.03125 v 2.734375 c 0,1.0625 0.859375,1.28125 1.578125,1.28125 0.75,0 1.203125,-0.578125 1.203125,-1.296875 z m 0,0"
+ id="path127" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph2-8">
+ <path
+ style="stroke:none"
+ d="m 8.390625,-6.375 v -0.46875 l -1.125,0.03125 c -0.390625,0 -0.921875,0 -1.296875,-0.03125 V -6.375 c 0.078125,0 0.875,0 0.875,0.125 0,0.046875 -0.03125,0.09375 -0.046875,0.125 L 4.78125,-1.59375 2.65625,-6.375 h 0.9375 v -0.46875 c -0.375,0.03125 -1.328125,0.03125 -1.765625,0.03125 -0.375,0 -1.21875,0 -1.5625,-0.03125 V -6.375 h 0.90625 l 2.75,6.203125 c 0.078125,0.171875 0.125,0.25 0.40625,0.25 0.15625,0 0.28125,0 0.390625,-0.234375 l 2.65625,-6 C 7.4375,-6.28125 7.484375,-6.375 8.203125,-6.375 Z m 0,0"
+ id="path130" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph2-9">
+ <path
+ style="stroke:none"
+ d="M 2.84375,0 V -0.46875 H 2.234375 V -4.484375 L 0.5,-4.40625 v 0.46875 c 0.59375,0 0.65625,0 0.65625,0.390625 V -0.46875 H 0.46875 V 0 L 1.6875,-0.03125 Z M 2.375,-6.046875 c 0,-0.4375 -0.34375,-0.78125 -0.78125,-0.78125 -0.421875,0 -0.78125,0.34375 -0.78125,0.78125 0,0.421875 0.359375,0.765625 0.78125,0.765625 0.4375,0 0.78125,-0.34375 0.78125,-0.765625 z m 0,0"
+ id="path133" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph2-10">
+ <path
+ style="stroke:none"
+ d="M 4.765625,-1.171875 C 4.765625,-1.3125 4.625,-1.3125 4.53125,-1.3125 c -0.1875,0 -0.1875,0.03125 -0.25,0.15625 -0.25,0.625 -0.734375,0.8125 -1.234375,0.8125 -1.390625,0 -1.390625,-1.453125 -1.390625,-1.921875 0,-0.5625 0,-1.84375 1.28125,-1.84375 0.359375,0 0.515625,0.015625 0.65625,0.046875 -0.1875,0.171875 -0.203125,0.375 -0.203125,0.46875 0,0.4375 0.34375,0.625 0.609375,0.625 0.3125,0 0.640625,-0.21875 0.640625,-0.625 0,-0.859375 -1.15625,-0.921875 -1.734375,-0.921875 -1.796875,0 -2.53125,1.140625 -2.53125,2.296875 0,1.328125 0.9375,2.28125 2.46875,2.28125 1.625,0 1.921875,-1.15625 1.921875,-1.234375 z m 0,0"
+ id="path136" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph3-0">
+ <path
+ style="stroke:none"
+ d=""
+ id="path139" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph3-1">
+ <path
+ style="stroke:none"
+ d="m 6.203125,-0.71875 c 0,-0.046875 0,-0.15625 -0.125,-0.15625 -0.125,0 -0.125,0.09375 -0.125,0.140625 -0.046875,0.5 -0.3125,0.671875 -0.546875,0.671875 -0.421875,0 -0.46875,-0.359375 -0.609375,-1.375 -0.0625,-0.453125 -0.140625,-1 -1.015625,-1.265625 0.625,-0.171875 1.375,-0.625 1.375,-1.3125 0,-0.78125 -1,-1.421875 -2.1875,-1.421875 H 0.359375 v 0.265625 h 0.1875 c 0.609375,0 0.625,0.078125 0.625,0.375 v 4.15625 c 0,0.296875 -0.015625,0.375 -0.625,0.375 h -0.1875 V 0 L 1.515625,-0.03125 2.6875,0 V -0.265625 H 2.515625 c -0.625,0 -0.640625,-0.078125 -0.640625,-0.375 v -1.96875 h 1.015625 c 0.578125,0 0.84375,0.296875 0.90625,0.359375 0.234375,0.25 0.234375,0.40625 0.234375,0.9375 0,0.5 0,0.84375 0.328125,1.140625 0.34375,0.296875 0.78125,0.34375 1.015625,0.34375 0.671875,0 0.828125,-0.65625 0.828125,-0.890625 z m -1.875,-3.296875 c 0,0.890625 -0.625,1.171875 -1.46875,1.171875 H 1.875 v -2.015625 c 0,-0.203125 0.015625,-0.28125 0.203125,-0.3125 0.078125,0 0.328125,0 0.484375,0 0.71875,0 1.765625,0 1.765625,1.15625 z m 0,0"
+ id="path142" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph3-2">
+ <path
+ style="stroke:none"
+ d="M 6.046875,0 V -0.265625 H 5.90625 c -0.5,0 -0.578125,-0.0625 -0.671875,-0.328125 L 3.375,-5.515625 C 3.328125,-5.625 3.3125,-5.6875 3.171875,-5.6875 3.03125,-5.6875 3,-5.625 2.96875,-5.515625 l -1.78125,4.6875 c -0.078125,0.21875 -0.25,0.5625 -0.90625,0.5625 V 0 c 0.265625,-0.03125 0.6875,-0.03125 0.828125,-0.03125 0.25,0 0.5,0 0.875,0.03125 v -0.265625 c -0.34375,0 -0.546875,-0.171875 -0.546875,-0.390625 0,-0.0625 0,-0.078125 0.03125,-0.171875 l 0.375,-1 h 2.171875 l 0.453125,1.1875 C 4.5,-0.546875 4.5,-0.5 4.5,-0.5 c 0,0.234375 -0.40625,0.234375 -0.640625,0.234375 V 0 L 5,-0.03125 c 0.4375,0 0.59375,0 1.046875,0.03125 z M 3.90625,-2.09375 H 1.9375 l 1,-2.59375 z m 0,0"
+ id="path145" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph3-3">
+ <path
+ style="stroke:none"
+ d="M 7.359375,0 V -0.265625 H 7.1875 c -0.625,0 -0.640625,-0.078125 -0.640625,-0.375 v -4.15625 c 0,-0.296875 0.015625,-0.375 0.640625,-0.375 H 7.359375 V -5.4375 h -1.34375 c -0.21875,0 -0.234375,0.015625 -0.296875,0.15625 L 3.875,-0.75 2.03125,-5.265625 C 1.953125,-5.421875 1.953125,-5.4375 1.734375,-5.4375 h -1.34375 v 0.265625 H 0.5625 c 0.609375,0 0.625,0.078125 0.625,0.375 v 3.9375 c 0,0.21875 0,0.59375 -0.796875,0.59375 V 0 C 0.75,-0.03125 1.125,-0.03125 1.328125,-0.03125 c 0.203125,0 0.578125,0 0.9375,0.03125 v -0.265625 c -0.796875,0 -0.796875,-0.375 -0.796875,-0.59375 V -5.09375 L 3.484375,-0.1875 C 3.53125,-0.09375 3.5625,0 3.671875,0 3.78125,0 3.8125,-0.09375 3.859375,-0.1875 l 2.03125,-4.96875 v 4.515625 c 0,0.296875 -0.015625,0.375 -0.625,0.375 H 5.09375 V 0 l 1.125,-0.03125 z m 0,0"
+ id="path148" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph3-4">
+ <path
+ style="stroke:none"
+ d="m 2.078125,0 v -0.265625 c -0.53125,0 -0.5625,-0.03125 -0.5625,-0.34375 v -2.90625 l -1.15625,0.09375 v 0.265625 c 0.515625,0 0.578125,0.046875 0.578125,0.4375 V -0.625 c 0,0.359375 -0.09375,0.359375 -0.609375,0.359375 V 0 c 0.3125,-0.03125 0.765625,-0.03125 0.890625,-0.03125 0.09375,0 0.578125,0 0.859375,0.03125 z M 1.625,-4.796875 C 1.625,-5.0625 1.40625,-5.25 1.171875,-5.25 c -0.21875,0 -0.4375,0.1875 -0.4375,0.453125 0,0.234375 0.1875,0.4375 0.4375,0.4375 0.25,0 0.453125,-0.203125 0.453125,-0.4375 z m 0,0"
+ id="path151" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph3-5">
+ <path
+ style="stroke:none"
+ d="m 4.484375,0 v -0.265625 c -0.515625,0 -0.609375,0 -0.609375,-0.359375 v -1.796875 c 0,-0.65625 -0.3125,-1.09375 -1.140625,-1.09375 -0.796875,0 -1.15625,0.578125 -1.25,0.765625 v -0.765625 l -1.15625,0.09375 v 0.265625 c 0.546875,0 0.609375,0.046875 0.609375,0.4375 V -0.625 c 0,0.359375 -0.09375,0.359375 -0.609375,0.359375 V 0 c 0.34375,-0.03125 0.6875,-0.03125 0.90625,-0.03125 0.234375,0 0.5625,0 0.90625,0.03125 v -0.265625 c -0.5,0 -0.609375,0 -0.609375,-0.359375 v -1.4375 c 0,-0.84375 0.640625,-1.234375 1.125,-1.234375 0.484375,0 0.609375,0.34375 0.609375,0.84375 V -0.625 c 0,0.359375 -0.09375,0.359375 -0.609375,0.359375 V 0 C 3,-0.03125 3.359375,-0.03125 3.5625,-0.03125 c 0.234375,0 0.578125,0 0.921875,0.03125 z m 0,0"
+ id="path154" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph3-6">
+ <path
+ style="stroke:none"
+ d="m 3.046875,-1.03125 c 0,-0.375 -0.21875,-0.9375 -1.171875,-1.109375 -0.0625,-0.015625 -0.515625,-0.09375 -0.546875,-0.09375 -0.25,-0.0625 -0.625,-0.234375 -0.625,-0.546875 0,-0.234375 0.1875,-0.578125 0.9375,-0.578125 0.890625,0 0.9375,0.65625 0.953125,0.875 0,0.0625 0.0625,0.09375 0.109375,0.09375 0.140625,0 0.140625,-0.0625 0.140625,-0.203125 v -0.75 c 0,-0.125 0,-0.203125 -0.109375,-0.203125 -0.046875,0 -0.0625,0 -0.1875,0.125 -0.015625,0 -0.09375,0.078125 -0.109375,0.078125 0,0 -0.03125,0 -0.078125,-0.03125 C 2.234375,-3.46875 2,-3.546875 1.640625,-3.546875 c -1.109375,0 -1.359375,0.59375 -1.359375,0.984375 0,0.390625 0.296875,0.625 0.3125,0.65625 0.328125,0.234375 0.5,0.265625 1.046875,0.359375 0.375,0.078125 0.984375,0.1875 0.984375,0.71875 0,0.3125 -0.203125,0.6875 -0.9375,0.6875 -0.8125,0 -1.046875,-0.625 -1.140625,-1.046875 C 0.515625,-1.296875 0.5,-1.328125 0.40625,-1.328125 c -0.125,0 -0.125,0.0625 -0.125,0.21875 V -0.125 c 0,0.125 0,0.203125 0.09375,0.203125 0.0625,0 0.0625,0 0.203125,-0.15625 C 0.625,-0.125 0.703125,-0.21875 0.75,-0.265625 1.109375,0.0625 1.484375,0.078125 1.6875,0.078125 2.703125,0.078125 3.046875,-0.5 3.046875,-1.03125 Z m 0,0"
+ id="path157" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph3-7">
+ <path
+ style="stroke:none"
+ d="m 3.515625,-0.953125 c 0,-0.03125 -0.03125,-0.109375 -0.125,-0.109375 -0.09375,0 -0.109375,0.046875 -0.125,0.09375 -0.28125,0.78125 -0.96875,0.796875 -1.109375,0.796875 -0.359375,0 -0.734375,-0.15625 -0.96875,-0.53125 C 0.953125,-1.0625 0.953125,-1.578125 0.953125,-1.8125 h 2.34375 c 0.171875,0 0.21875,0 0.21875,-0.1875 C 3.515625,-2.703125 3.125,-3.546875 2,-3.546875 c -0.984375,0 -1.765625,0.8125 -1.765625,1.796875 0,1.03125 0.859375,1.828125 1.875,1.828125 1,0 1.40625,-0.84375 1.40625,-1.03125 z M 2.96875,-2.03125 H 0.953125 C 1.03125,-3.140625 1.703125,-3.328125 2,-3.328125 c 0.9375,0 0.96875,1.125 0.96875,1.296875 z m 0,0"
+ id="path160" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph3-8">
+ <path
+ style="stroke:none"
+ d="m 3.0625,-3.015625 c 0,-0.28125 -0.25,-0.5 -0.609375,-0.5 -0.515625,0 -0.875,0.390625 -1.03125,0.84375 H 1.40625 v -0.84375 l -1.125,0.09375 v 0.265625 c 0.546875,0 0.609375,0.046875 0.609375,0.4375 V -0.625 c 0,0.359375 -0.109375,0.359375 -0.609375,0.359375 V 0 c 0.3125,-0.03125 0.75,-0.03125 0.9375,-0.03125 0.46875,0 0.484375,0 1,0.03125 V -0.265625 H 2.0625 c -0.578125,0 -0.59375,-0.078125 -0.59375,-0.375 V -1.8125 c 0,-0.609375 0.25,-1.46875 1.015625,-1.484375 -0.046875,0.03125 -0.140625,0.09375 -0.140625,0.28125 0,0.25 0.203125,0.359375 0.359375,0.359375 0.1875,0 0.359375,-0.125 0.359375,-0.359375 z m 0,0"
+ id="path163" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph3-9">
+ <path
+ style="stroke:none"
+ d="m 2.8125,-1 v -0.4375 h -0.25 v 0.421875 c 0,0.546875 -0.25,0.84375 -0.546875,0.84375 -0.53125,0 -0.53125,-0.6875 -0.53125,-0.8125 v -2.1875 h 1.1875 V -3.4375 h -1.1875 v -1.46875 h -0.25 c 0,0.734375 -0.328125,1.484375 -1.078125,1.515625 v 0.21875 H 0.875 V -1 c 0,0.9375 0.71875,1.078125 1.078125,1.078125 C 2.5,0.078125 2.8125,-0.390625 2.8125,-1 Z m 0,0"
+ id="path166" />
+ </symbol>
+ <symbol
+ overflow="visible"
+ id="glyph3-10">
+ <path
+ style="stroke:none"
+ d="m 3.984375,-1.703125 c 0,-0.984375 -0.828125,-1.84375 -1.875,-1.84375 -1.046875,0 -1.875,0.859375 -1.875,1.84375 0,1 0.859375,1.78125 1.875,1.78125 1.03125,0 1.875,-0.78125 1.875,-1.78125 z m -0.703125,-0.0625 c 0,0.359375 -0.015625,0.796875 -0.25,1.140625 -0.203125,0.3125 -0.5625,0.453125 -0.921875,0.453125 -0.421875,0 -0.765625,-0.203125 -0.9375,-0.484375 -0.203125,-0.328125 -0.21875,-0.71875 -0.21875,-1.109375 0,-0.3125 0,-0.78125 0.234375,-1.125 0.21875,-0.28125 0.546875,-0.4375 0.921875,-0.4375 0.421875,0 0.765625,0.203125 0.9375,0.46875 0.21875,0.34375 0.234375,0.765625 0.234375,1.09375 z m 0,0"
+ id="path169" />
+ </symbol>
+ </g>
+ <clipPath
+ id="clip1">
+ <path
+ d="M 6,0 H 315.60937 V 71 H 6 Z m 0,0"
+ id="path174" />
+ </clipPath>
+ <clipPath
+ id="clip2">
+ <path
+ d="m 6,85 h 309.60937 v 39.71875 H 6 Z m 0,0"
+ id="path177" />
+ </clipPath>
+ <clipPath
+ id="clip3">
+ <path
+ d="m 133,87 h 47 v 37.71875 h -47 z m 0,0"
+ id="path180" />
+ </clipPath>
+ </defs>
+ <g
+ id="surface10254"
+ transform="translate(-6.636719)">
+ <g
+ clip-path="url(#clip1)"
+ clip-rule="nonzero"
+ id="g187">
+ <path
+ style="fill:#bdb8d9;fill-opacity:1;fill-rule:nonzero;stroke:none"
+ d="M 6.636719,67.875 V 2.984375 c 0,-1.652344 1.335937,-2.98828125 2.988281,-2.98828125 h 303 c 1.65234,0 2.98828,1.33593725 2.98828,2.98828125 V 67.875 c 0,1.648438 -1.33594,2.988281 -2.98828,2.988281 h -303 c -1.652344,0 -2.988281,-1.339843 -2.988281,-2.988281 z m 0,0"
+ id="path185" />
+ </g>
+ <g
+ clip-path="url(#clip2)"
+ clip-rule="nonzero"
+ id="g191">
+ <path
+ style="fill:#8cd1c5;fill-opacity:1;fill-rule:nonzero;stroke:none"
+ d="m 6.636719,88.023438 v 33.707032 c 0,1.65234 1.335937,2.99219 2.988281,2.99219 h 303 c 1.65234,0 2.98828,-1.33985 2.98828,-2.99219 V 88.023438 c 0,-1.648438 -1.33594,-2.988282 -2.98828,-2.988282 h -303 c -1.652344,0 -2.988281,1.339844 -2.988281,2.988282 z m 0,0"
+ id="path189" />
+ </g>
+ <path
+ style="fill:#ffffff;fill-opacity:1;fill-rule:nonzero;stroke:none"
+ d="M 40.234375,46.769531 H 12.722656 c -1.652344,0 -2.988281,1.335938 -2.988281,2.988281 v 13.863282 c 0,1.652344 1.335937,2.988281 2.988281,2.988281 h 27.511719 c 1.652344,0 2.988281,-1.335937 2.988281,-2.988281 V 49.757812 c 0,-1.652343 -1.335937,-2.988281 -2.988281,-2.988281 z m 0,0"
+ id="path193" />
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g205">
+ <use
+ xlink:href="#glyph0-1"
+ x="13.053"
+ y="59.174999"
+ id="use195"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-2"
+ x="20.245996"
+ y="59.174999"
+ id="use197"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-3"
+ x="23.0156"
+ y="59.174999"
+ id="use199"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-4"
+ x="25.785204"
+ y="59.174999"
+ id="use201"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-5"
+ x="30.766502"
+ y="59.174999"
+ id="use203"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g209">
+ <use
+ xlink:href="#glyph0-6"
+ x="36.026756"
+ y="59.174999"
+ id="use207"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g213">
+ <use
+ xlink:href="#glyph1-1"
+ x="57.516998"
+ y="58.903"
+ id="use211"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g217">
+ <use
+ xlink:href="#glyph1-1"
+ x="61.930431"
+ y="58.903"
+ id="use215"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g221">
+ <use
+ xlink:href="#glyph1-1"
+ x="66.353828"
+ y="58.903"
+ id="use219"
+ width="100%"
+ height="100%" />
+ </g>
+ <path
+ style="fill:#ffffff;fill-opacity:1;fill-rule:nonzero;stroke:none"
+ d="M 134.55859,46.769531 H 88.476562 c -1.652343,0 -2.988281,1.335938 -2.988281,2.988281 v 13.863282 c 0,1.652344 1.335938,2.988281 2.988281,2.988281 h 46.082028 c 1.65235,0 2.99219,-1.335937 2.99219,-2.988281 V 49.757812 c 0,-1.652343 -1.33984,-2.988281 -2.99219,-2.988281 z m 0,0"
+ id="path223" />
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g243">
+ <use
+ xlink:href="#glyph0-1"
+ x="88.807999"
+ y="60.091"
+ id="use225"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-7"
+ x="96.000999"
+ y="60.091"
+ id="use227"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-3"
+ x="104.29984"
+ y="60.091"
+ id="use229"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-8"
+ x="107.06944"
+ y="60.091"
+ id="use231"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-9"
+ x="112.60865"
+ y="60.091"
+ id="use233"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-10"
+ x="117.58995"
+ y="60.091"
+ id="use235"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-11"
+ x="121.49529"
+ y="60.091"
+ id="use237"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-12"
+ x="127.03449"
+ y="60.091"
+ id="use239"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-2"
+ x="131.45789"
+ y="60.091"
+ id="use241"
+ width="100%"
+ height="100%" />
+ </g>
+ <path
+ style="fill:#ffffff;fill-opacity:1;fill-rule:nonzero;stroke:none"
+ d="m 178.22656,46.769531 h -20.03125 c -1.64844,0 -2.98828,1.335938 -2.98828,2.988281 v 13.863282 c 0,1.652344 1.33984,2.988281 2.98828,2.988281 h 20.03125 c 1.65235,0 2.98828,-1.335937 2.98828,-2.988281 V 49.757812 c 0,-1.652343 -1.33593,-2.988281 -2.98828,-2.988281 z m 0,0"
+ id="path245" />
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g251">
+ <use
+ xlink:href="#glyph0-13"
+ x="158.528"
+ y="60.146"
+ id="use247"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-14"
+ x="163.50929"
+ y="60.146"
+ id="use249"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g255">
+ <use
+ xlink:href="#glyph0-1"
+ x="170.7023"
+ y="60.146"
+ id="use253"
+ width="100%"
+ height="100%" />
+ </g>
+ <path
+ style="fill:#ffffff;fill-opacity:1;fill-rule:nonzero;stroke:none"
+ d="m 220.47266,46.769531 h -19.48047 c -1.65235,0 -2.99219,1.335938 -2.99219,2.988281 v 13.863282 c 0,1.652344 1.33984,2.988281 2.99219,2.988281 h 19.48047 c 1.65234,0 2.98828,-1.335937 2.98828,-2.988281 V 49.757812 c 0,-1.652343 -1.33594,-2.988281 -2.98828,-2.988281 z m 0,0"
+ id="path257" />
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g261">
+ <use
+ xlink:href="#glyph0-15"
+ x="201.32201"
+ y="60.091"
+ id="use259"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g267">
+ <use
+ xlink:href="#glyph0-16"
+ x="206.72173"
+ y="60.091"
+ id="use263"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-15"
+ x="213.91472"
+ y="60.091"
+ id="use265"
+ width="100%"
+ height="100%" />
+ </g>
+ <path
+ style="fill:#ffffff;fill-opacity:1;fill-rule:nonzero;stroke:none"
+ d="m 310.46094,46.769531 h -34.17969 c -1.64844,0 -2.98828,1.335938 -2.98828,2.988281 v 13.863282 c 0,1.652344 1.33984,2.988281 2.98828,2.988281 h 34.17969 c 1.65234,0 2.98828,-1.335937 2.98828,-2.988281 V 49.757812 c 0,-1.652343 -1.33594,-2.988281 -2.98828,-2.988281 z m 0,0"
+ id="path269" />
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g279">
+ <use
+ xlink:href="#glyph0-17"
+ x="276.61499"
+ y="60.036999"
+ id="use271"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-17"
+ x="281.59631"
+ y="60.036999"
+ id="use273"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-10"
+ x="286.57761"
+ y="60.036999"
+ id="use275"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-18"
+ x="290.48294"
+ y="60.036999"
+ id="use277"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g287">
+ <use
+ xlink:href="#glyph0-5"
+ x="294.62738"
+ y="60.036999"
+ id="use281"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-19"
+ x="300.1666"
+ y="60.036999"
+ id="use283"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-20"
+ x="305.14789"
+ y="60.036999"
+ id="use285"
+ width="100%"
+ height="100%" />
+ </g>
+ <path
+ style="fill:#ffffff;fill-opacity:1;fill-rule:nonzero;stroke:none"
+ d="m 292.16797,24.089844 h -15.88672 c -1.64844,0 -2.98828,1.339844 -2.98828,2.988281 v 13.867187 c 0,1.648438 1.33984,2.988282 2.98828,2.988282 h 15.88672 c 1.65234,0 2.99219,-1.339844 2.99219,-2.988282 V 27.078125 c 0,-1.648437 -1.33985,-2.988281 -2.99219,-2.988281 z m 0,0"
+ id="path289" />
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g297">
+ <use
+ xlink:href="#glyph0-21"
+ x="276.61499"
+ y="37.220001"
+ id="use291"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-22"
+ x="281.87524"
+ y="37.220001"
+ id="use293"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-19"
+ x="286.85657"
+ y="37.220001"
+ id="use295"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g301">
+ <use
+ xlink:href="#glyph1-1"
+ x="276.61499"
+ y="19.218"
+ id="use299"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g305">
+ <use
+ xlink:href="#glyph1-1"
+ x="281.02844"
+ y="19.218"
+ id="use303"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g309">
+ <use
+ xlink:href="#glyph1-1"
+ x="285.45181"
+ y="19.218"
+ id="use307"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g313">
+ <use
+ xlink:href="#glyph1-1"
+ x="236.10201"
+ y="58.903"
+ id="use311"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g317">
+ <use
+ xlink:href="#glyph1-1"
+ x="240.51543"
+ y="58.903"
+ id="use315"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g321">
+ <use
+ xlink:href="#glyph1-1"
+ x="244.93883"
+ y="58.903"
+ id="use319"
+ width="100%"
+ height="100%" />
+ </g>
+ <path
+ style="fill:#ffffff;fill-opacity:1;fill-rule:nonzero;stroke:none"
+ d="m 178.98828,89.289062 h -21.55469 c -1.64843,0 -2.98828,1.335938 -2.98828,2.988282 v 13.863286 c 0,1.65234 1.33985,2.98828 2.98828,2.98828 h 21.55469 c 1.65234,0 2.98828,-1.33594 2.98828,-2.98828 V 92.277344 c 0,-1.652344 -1.33594,-2.988282 -2.98828,-2.988282 z m 0,0"
+ id="path323" />
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g331">
+ <use
+ xlink:href="#glyph0-23"
+ x="157.76601"
+ y="102.611"
+ id="use325"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-16"
+ x="165.23795"
+ y="102.611"
+ id="use327"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-15"
+ x="172.43095"
+ y="102.611"
+ id="use329"
+ width="100%"
+ height="100%" />
+ </g>
+ <path
+ style="fill:#ffffff;fill-opacity:1;fill-rule:nonzero;stroke:none"
+ d="m 240.47656,89.289062 h -31.14062 c -1.65235,0 -2.98828,1.335938 -2.98828,2.988282 v 13.863286 c 0,1.65234 1.33593,2.98828 2.98828,2.98828 h 31.14062 c 1.64844,0 2.98828,-1.33594 2.98828,-2.98828 V 92.277344 c 0,-1.652344 -1.33984,-2.988282 -2.98828,-2.988282 z m 0,0"
+ id="path333" />
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g337">
+ <use
+ xlink:href="#glyph0-24"
+ x="209.66701"
+ y="101.64"
+ id="use335"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g351">
+ <use
+ xlink:href="#glyph0-12"
+ x="216.31206"
+ y="101.64"
+ id="use339"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-10"
+ x="220.73544"
+ y="101.64"
+ id="use341"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-3"
+ x="224.64079"
+ y="101.64"
+ id="use343"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-2"
+ x="227.41039"
+ y="101.64"
+ id="use345"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-9"
+ x="230.17999"
+ y="101.64"
+ id="use347"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph0-4"
+ x="235.16129"
+ y="101.64"
+ id="use349"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g369">
+ <use
+ xlink:href="#glyph2-1"
+ x="12.99"
+ y="13.84"
+ id="use353"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph2-2"
+ x="21.268921"
+ y="13.84"
+ id="use355"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph2-3"
+ x="26.997416"
+ y="13.84"
+ id="use357"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph2-4"
+ x="36.541588"
+ y="13.84"
+ id="use359"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph2-1"
+ x="42.907688"
+ y="13.84"
+ id="use361"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph2-5"
+ x="51.186607"
+ y="13.84"
+ id="use363"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph2-6"
+ x="56.436897"
+ y="13.84"
+ id="use365"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph2-7"
+ x="61.159172"
+ y="13.84"
+ id="use367"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g373">
+ <use
+ xlink:href="#glyph2-8"
+ x="12.99"
+ y="99.751999"
+ id="use371"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g389">
+ <use
+ xlink:href="#glyph2-5"
+ x="20.69109"
+ y="99.751999"
+ id="use375"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph2-6"
+ x="25.94138"
+ y="99.751999"
+ id="use377"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph2-9"
+ x="30.663652"
+ y="99.751999"
+ id="use379"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph2-10"
+ x="33.841721"
+ y="99.751999"
+ id="use381"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph2-5"
+ x="38.93261"
+ y="99.751999"
+ id="use383"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph2-6"
+ x="44.182899"
+ y="99.751999"
+ id="use385"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph2-7"
+ x="48.905174"
+ y="99.751999"
+ id="use387"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g397">
+ <use
+ xlink:href="#glyph3-1"
+ x="115.526"
+ y="112.701"
+ id="use391"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph3-2"
+ x="121.75862"
+ y="112.701"
+ id="use393"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph3-3"
+ x="128.10281"
+ y="112.701"
+ id="use395"
+ width="100%"
+ height="100%" />
+ </g>
+ <g
+ style="fill:#000000;fill-opacity:1"
+ id="g417">
+ <use
+ xlink:href="#glyph3-4"
+ x="109.676"
+ y="119.675"
+ id="use399"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph3-5"
+ x="112.02718"
+ y="119.675"
+ id="use401"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph3-6"
+ x="116.72954"
+ y="119.675"
+ id="use403"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph3-7"
+ x="120.06901"
+ y="119.675"
+ id="use405"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph3-8"
+ x="123.83089"
+ y="119.675"
+ id="use407"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph3-9"
+ x="127.13052"
+ y="119.675"
+ id="use409"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph3-4"
+ x="130.42216"
+ y="119.675"
+ id="use411"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph3-10"
+ x="132.77335"
+ y="119.675"
+ id="use413"
+ width="100%"
+ height="100%" />
+ <use
+ xlink:href="#glyph3-5"
+ x="137.00548"
+ y="119.675"
+ id="use415"
+ width="100%"
+ height="100%" />
+ </g>
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1"
+ d="m 8.439875,0.0015 h 9.777344"
+ transform="matrix(1,0,0,-1,34.982,56.689)"
+ id="path419" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:10;stroke-opacity:1"
+ d="M -2.552025,3.110875 C -2.083275,1.243687 -1.044213,0.364781 -0.00124375,0.0015 -1.044213,-0.361781 -2.083275,-1.244594 -2.552025,-3.111781"
+ transform="matrix(1,0,0,-1,53.5989,56.689)"
+ id="path421" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1"
+ d="M 37.678156,0.0015 H 49.510188"
+ transform="matrix(1,0,0,-1,34.982,56.689)"
+ id="path423" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:10;stroke-opacity:1"
+ d="M -2.549976,3.110875 C -2.085132,1.243687 -1.04607,0.364781 8.05e-4,0.0015 -1.04607,-0.361781 -2.085132,-1.244594 -2.549976,-3.111781"
+ transform="matrix(1,0,0,-1,84.88982,56.689)"
+ id="path425" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1"
+ d="m 102.768,0.0015 h 16.46094"
+ transform="matrix(1,0,0,-1,34.982,56.689)"
+ id="path427" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:10;stroke-opacity:1"
+ d="M -2.551166,3.110875 C -2.086322,1.243687 -1.04726,0.364781 -3.85e-4,0.0015 -1.04726,-0.361781 -2.086322,-1.244594 -2.551166,-3.111781"
+ transform="matrix(1,0,0,-1,154.60976,56.689)"
+ id="path429" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1"
+ d="m 146.43206,0.0015 h 15.58985"
+ transform="matrix(1,0,0,-1,34.982,56.689)"
+ id="path431" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:10;stroke-opacity:1"
+ d="M -2.552408,3.110875 C -2.083658,1.243687 -1.044595,0.364781 -0.00162625,0.0015 -1.044595,-0.361781 -2.083658,-1.244594 -2.552408,-3.111781"
+ transform="matrix(1,0,0,-1,197.40397,56.689)"
+ id="path433" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1"
+ d="m 188.67816,0.0015 h 8.125"
+ transform="matrix(1,0,0,-1,34.982,56.689)"
+ id="path435" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:10;stroke-opacity:1"
+ d="M -2.551057,3.110875 C -2.086214,1.243687 -1.047151,0.364781 -2.7625e-4,0.0015 -1.047151,-0.361781 -2.086214,-1.244594 -2.551057,-3.111781"
+ transform="matrix(1,0,0,-1,232.18387,56.689)"
+ id="path437" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1"
+ d="m 216.26409,0.0015 h 21.05078"
+ transform="matrix(1,0,0,-1,34.982,56.689)"
+ id="path439" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:10;stroke-opacity:1"
+ d="M -2.551979,3.110875 C -2.083229,1.243687 -1.048072,0.364781 -0.0011975,0.0015 -1.048072,-0.361781 -2.083229,-1.244594 -2.551979,-3.111781"
+ transform="matrix(1,0,0,-1,272.69651,56.689)"
+ id="path441" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1"
+ d="m 216.26409,0.0015 c 12.28516,0 10.30469,18.472656 21.10157,22.402344"
+ transform="matrix(1,0,0,-1,34.982,56.689)"
+ id="path443" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:10;stroke-opacity:1"
+ d="M -2.549132,3.109508 C -2.084774,1.244442 -1.046101,0.363405 -0.00193857,-4.77835e-6 -1.044977,-0.364479 -2.084828,-1.245581 -2.550933,-3.108709"
+ transform="matrix(0.93968,-0.34201,-0.34201,-0.93968,272.72057,34.14777)"
+ id="path445" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1"
+ d="m 216.26409,0.0015 c 17.67578,0 4.44141,36.613281 21.0625,39.546875"
+ transform="matrix(1,0,0,-1,34.982,56.689)"
+ id="path447" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:10;stroke-opacity:1"
+ d="M -2.549055,3.109583 C -2.084879,1.242801 -1.046318,0.361581 3.08915e-4,-0.00144434 -1.047336,-0.364117 -2.083134,-1.244529 -2.550801,-3.109646"
+ transform="matrix(0.9848,-0.17363,-0.17363,-0.9848,272.70257,17.07285)"
+ id="path449" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1"
+ d="M 133.22894,-10.119594 V -31.603969"
+ transform="matrix(1,0,0,-1,34.982,56.689)"
+ id="path451" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:10;stroke-opacity:1"
+ d="m -2.549445,3.112319 c 0.464844,-1.867188 1.503906,-2.75 2.55078125,-3.1132815 C -1.045539,-0.364244 -2.084601,-1.24315 -2.549445,-3.110337"
+ transform="matrix(0,1,1,0,168.2119,88.69007)"
+ id="path453" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1"
+ d="m 147.19378,-42.521938 h 23.17578"
+ transform="matrix(1,0,0,-1,34.982,56.689)"
+ id="path455" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:10;stroke-opacity:1"
+ d="M -2.549931,3.111544 C -2.085087,1.244356 -1.046025,0.361544 8.5e-4,-0.0017375 -1.046025,-0.361113 -2.085087,-1.243925 -2.549931,-3.111113"
+ transform="matrix(1,0,0,-1,205.74915,99.2092)"
+ id="path457" />
+ <g
+ clip-path="url(#clip3)"
+ clip-rule="nonzero"
+ id="g461">
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1"
+ d="m 119.26409,-42.521938 c -8.08593,0 -12.8789,-15.800781 -5.875,-19.839843 7.48438,-4.324219 19.83985,1.074218 19.83985,8.925781"
+ transform="matrix(1,0,0,-1,34.982,56.689)"
+ id="path459" />
+ </g>
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.79701;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:10;stroke-opacity:1"
+ d="M -2.549004,3.110337 C -2.08416,1.24315 -1.045097,0.364244 0.0017775,9.625e-4 -1.045097,-0.362319 -2.08416,-1.245131 -2.549004,-3.112319"
+ transform="matrix(0,-1,-1,0,168.2119,109.72834)"
+ id="path463" />
+ </g>
+</svg>
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. <tactics> Qed.= is <= 80 characters) can go all in one line.
+
+- When ending a proof, align the ending statement (=Qed=, =Admitted=, etc.) with =Proof=.
+
+- Avoid referring to autogenerated names (e.g. =H0=, =n0=). It's okay to let Coq generate these names,
+ but you should not explicitly refer to them in your proof. So =intros; my_solver= is fine, but
+ =intros; apply H1; my_solver= is not fine.
+
+ - You can force a non-autogenerated name by either putting the variable before the colon in the
+ lemma statement (=Lemma foo x : ...= instead of =Lemma foo : forall x, ...=), or by passing
+ arguments to =intros= (e.g. =intros ? x= to name the second argument =x=)
+
+- This way, the proof won't break when new hypotheses are added or autogenerated variable names
+ change.
+
+- Use curly braces ={}= for subgoals, instead of bullets.
+
+- /Never write tactics with more than one subgoal focused./ This can make the proof very confusing to
+ step through! If you have more than one subgoal, use curly braces.
+
+- Consider adding a comment after the opening curly brace that explains what case you're in (see
+ example).
+
+ - This is not necessary for small subgoals but can help show the major lines of reasoning in large
+ proofs.
+
+- If invoking a tactic that is expected to return multiple subgoals, use =[ | ... | ]= before the =.= to
+ explicitly specify how many subgoals you expect.
+
+ - Examples: =split; [ | ].= =induction z; [ | | ].=
+ - This helps make code more maintainable, because it fails immediately if your tactic no longer
+ solves as many subgoals as expected (or unexpectedly solves more).
+
+- If invoking a string of tactics (composed by =;=) that will break the goal into multiple subgoals
+ and then solve all but one, still use =[ ]= to enforce that all but one goal is solved.
+
+ - Example: =split; try lia; [ ]=.
+
+- Tactics that consist only of =repeat=-ing a procedure (e.g. =repeat match=, =repeat first=) should
+ factor out a single step of that procedure a separate tactic called =<tactic name>_step=, because
+ the single-step version is much easier to debug. For instance:
+
+ #+begin_src coq
+ Ltac crush_step :=
+ match goal with
+ | _ => progress subst
+ | _ => reflexivity
+ end.
+ Ltac crush := repeat crush_step.
+ #+end_src
+
+** Naming
+ :PROPERTIES:
+ :CUSTOM_ID: naming
+ :END:
+
+- Helper proofs about standard library datatypes should go in a module that is named to match the
+ standard library module (see example).
+
+ - This makes the helper proofs look like standard-library ones, which is helpful for categorizing
+ them if they're genuinely at the standard-library level of abstraction.
+
+- Names of modules should start with capital letters.
+- Names of inductives and their constructors should start with capital letters.
+- Names of other definitions/lemmas should be snake case.
+
+** Example
+ :PROPERTIES:
+ :CUSTOM_ID: example
+ :END:
+A small standalone Coq file that exhibits many of the style points.
+
+#+begin_src coq
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2021 Name <email@example.com>
+ *
+ * <License...>
+ *)
+
+ Require Import Coq.Lists.List.
+ Require Import Coq.micromega.Lia.
+ Require Import Coq.ZArith.ZArith.
+ Import ListNotations.
+ Local Open Scope Z_scope.
+
+ (* Helper proofs about standard library integers (Z) go within [Module Z] so
+ that they match standard-library Z lemmas when used. *)
+ Module Z.
+ Lemma pow_3_r x : x ^ 3 = x * x * x.
+ Proof. lia. Qed. (* very short proofs can go all on one line *)
+
+ Lemma pow_4_r x : x ^ 4 = x * x * x * x.
+ Proof.
+ change 4 with (Z.succ (Z.succ (Z.succ (Z.succ 0)))).
+ repeat match goal with
+ | _ => rewrite Z.pow_1_r
+ | _ => rewrite Z.pow_succ_r by lia
+ | |- context [x * (?a * ?b)] =>
+ replace (x * (a * b)) with (a * b * x) by lia
+ | _ => reflexivity
+ end.
+ Qed.
+ End Z.
+ (* Now we can access the lemmas above as Z.pow_3_r and Z.pow_4_r, as if they
+ were in the ZArith library! *)
+
+ Definition bar (x y : Z) := x ^ (y + 1).
+
+ (* example with a painfully manual proof to show case formatting *)
+ Lemma bar_upper_bound :
+ forall x y a,
+ 0 <= x <= a -> 0 <= y ->
+ 0 <= bar x y <= a ^ (y + 1).
+ Proof.
+ (* avoid referencing autogenerated names by explicitly naming variables *)
+ intros x y a Hx Hy. revert y Hy x a Hx.
+ (* explicitly indicate # subgoals with [ | ... | ] if > 1 *)
+ cbv [bar]; refine (natlike_ind _ _ _); [ | ].
+ { (* y = 0 *)
+ intros; lia. }
+ { (* y = Z.succ _ *)
+ intros.
+ rewrite Z.add_succ_l, Z.pow_succ_r by lia.
+ split.
+ { (* 0 <= bar x y *)
+ apply Z.mul_nonneg_nonneg; [ lia | ].
+ apply Z.pow_nonneg; lia. }
+ { (* bar x y < a ^ y *)
+ rewrite Z.pow_succ_r by lia.
+ apply Z.mul_le_mono_nonneg; try lia;
+ [ apply Z.pow_nonneg; lia | ].
+ (* For more flexible proofs, use match statements to find hypotheses
+ rather than referring to them by autogenerated names like H0. In this
+ case, we'll take any hypothesis that applies to and then solves the
+ goal. *)
+ match goal with H : _ |- _ => apply H; solve [auto] end. } }
+ Qed.
+
+ (* Put notations in a separate module or file so that importers can
+ decide whether or not to use them. *)
+ Module BarNotations.
+ Infix "#" := bar (at level 40) : Z_scope.
+ Notation "x '##'" := (bar x x) (at level 40) : Z_scope.
+ End BarNotations.
+#+end_src
+
+* Index - Features
+:PROPERTIES:
+:CUSTOM_ID: cindex
+:APPENDIX: t
+:INDEX: cp
+:DESCRIPTION: Key concepts & features
+:END:
+
+* Export Setup :noexport:
+
+#+setupfile: common.org
+
+#+export_file_name: vericert.texi
+
+#+texinfo_dir_category: High-level synthesis tool
+#+texinfo_dir_title: Vericert
+#+texinfo_dir_desc: Formally verified high-level synthesis tool
+
+* GNU Free Documentation License
+:PROPERTIES:
+:appendix: t
+:END:
+
+#+include: res/fdl.org
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: <style>body{font-family:monospace;max-width:60em}h1{text-align:center}dt{font-weight:700}dd{margin-bottom:1em}</style>
+
+* 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 <dir> :: 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 <value> :: Generate code for the given target
+- -conf <file> :: Read configuration from file
+- @<file> :: Read command line options from <file>
+
+** Tracing Options:
+
+- -dprepro :: Save C file after preprocessing in <file>.i
+- -dparse :: Save C file after parsing and elaboration in <file>.parsed.c
+- -dc :: Save generated C in <file>.compcert.c
+- -dclight :: Save generated Clight in <file>.light.c
+- -dcminor :: Save generated Cminor in <file>.cm
+- -drtl :: Save RTL at various optimization points in <file>.rtl.<n>
+- -drtlblock :: Save RTLBlock <file>.rtlblock
+- -dhtl :: Save HTL before Verilog generation <file>.htl
+- -dltl :: Save LTL after register allocation in <file>.ltl
+- -dmach :: Save generated Mach code in <file>.mach
+- -dasm :: Save generated assembly in <file>.s
+- -dall :: Save all generated intermediate files in <file>.<ext>
+- -sdump :: Save info for post-linking validation in <file>.json
+- -o <file> :: Generate output in <file>
+
+** Diagnostic options:
+
+- -Wall :: Enable all warnings
+- -W<warning> :: Enable the specific <warning>
+- -Wno-<warning> :: Disable the specific <warning>
+- -Werror :: Make all warnings into errors
+- -Werror=<warning> :: Turn <warning> into an error
+- -Wno-error=<warning> :: Turn <warning> 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=<n> :: 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 <yann@yannherklotz.com>
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <https://www.gnu.org/licenses/>.
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 <https://compcert.org/compcert-C.html>`_ to perform this translation.
+
+.. index:: vericert
+
+.. _building:
+
+Building Vericert
+-----------------
+
+
+Testing
+~~~~~~~
+
+To test out ``vericert`` you can try the following examples which are in the test folder using the
+following:
+
+.. code:: shell
+
+ ./bin/vericert test/loop.c -o loop.v
+ ./bin/vericert test/conditional.c -o conditional.v
+ ./bin/vericert test/add.c -o add.v
+
+Or by running the test suite using the following command:
+
+.. code:: shell
+
+ make test
+
+.. _using-vericert:
+
+.. index:: vericert
+
+Using Vericert
+--------------
+
+Vericert can be used to translate a subset of C into Verilog. As a simple example, consider the
+following C file (``main.c``):
+
+.. code:: C
+
+ void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) {
+ int sum = 0;
+ for (int c = 0; c < 2; c++) {
+ for (int d = 0; d < 2; d++) {
+ for (int k = 0; k < 2; k++) {
+ sum = sum + first[c][k]*second[k][d];
+ }
+ multiply[c][d] = sum;
+ sum = 0;
+ }
+ }
+ }
+
+ int main() {
+ int f[2][2] = {{1, 2}, {3, 4}};
+ int s[2][2] = {{5, 6}, {7, 8}};
+ int m[2][2] = {{0, 0}, {0, 0}};
+
+ matrix_multiply(f, s, m);
+ return m[1][1];
+ }
+
+It can be compiled using the following command, assuming that vericert is somewhere on the path.
+
+.. code:: shell
+
+ vericert main.c -o main.v
+
+The Verilog file contains a top-level test-bench, which can be given to any Verilog simulator to
+simulate the hardware, which should give the same result as executing the C code. Using `Icarus
+Verilog <http://iverilog.icarus.com/>`_ as an example:
+
+.. code:: shell
+
+ iverilog -o main_v main.v
+
+When executing, it should therefore print the following:
+
+.. code:: shell
+
+ $ ./main_v
+ finished: 50
+
+This gives the same result as executing the C in the following way:
+
+.. code:: shell
+
+ $ gcc -o main_c main.c
+ $ ./main_c
+ $ echo $?
+ 50
+
+Man pages
+~~~~~~~~~
+
+.. _unreleased-features:
+
+Unreleased Features
+-------------------
+
+The following are unreleased features in Vericert that are currently being worked on and have not
+been completely proven correct yet. Currently this includes features such as:
+
+- `scheduling`_,
+
+- `operation-chaining`_,
+
+- `if-conversion`_, and
+
+- `functions`_.
+
+This page gives some preliminary information on how the features are implemented and how the proofs
+for the features are being done. Once these features are properly implemented, they will be added
+to the proper documentation.
+
+.. _scheduling:
+
+Scheduling
+~~~~~~~~~~
+
+Scheduling is an optimisation which is used to run various instructions in parallel that are
+independent to each other.
+
+.. _operation-chaining:
+
+Operation Chaining
+~~~~~~~~~~~~~~~~~~
+
+Operation chaining is an optimisation that can be added on to scheduling and allows for the
+sequential execution of instructions in a clock cycle, while executing other instructions in
+parallel in the same clock cycle.
+
+.. _if-conversion:
+
+If-conversion
+~~~~~~~~~~~~~
+
+If-conversion is an optimisation which can turn code with simple control flow into a single block
+(called a hyper-block), using predicated instructions.
+
+.. _functions:
+
+Functions
+~~~~~~~~~
+
+Functions are currently only inlined in Vericert, however, we are working on a proper interface to
+integrate function calls into the hardware.
+
+.. _coq-style-guide:
+
+Coq Style Guide
+---------------
+
+This style guide was taken from `Silveroak <https://github.com/project-oak/silveroak>`_, it outlines
+code style for Coq code in this repository. There are certainly other valid strategies and opinions
+on Coq code style; this is laid out purely in the name of consistency. For a visual example of the
+style, see the `example`_ at the bottom of this file.
+
+.. _code-organization:
+
+Code organization
+~~~~~~~~~~~~~~~~~
+
+.. _legal-banner:
+
+Legal banner
+^^^^^^^^^^^^
+
+- Files should begin with a copyright/license banner, as shown in the example above.
+
+.. _import-statements:
+
+Import statements
+^^^^^^^^^^^^^^^^^
+
+- ``Require Import`` statements should all go at the top of the file, followed by file-wide ``Import``
+ statements.
+
+ - =Import=s often contain notations or typeclass instances that might override notations or
+ instances from another library, so it’s nice to highlight them separately.
+
+- One ``Require Import`` statement per line; it’s easier to scan that way.
+
+- ``Require Import`` statements should use “fully-qualified” names (e.g. ``Require Import
+ Coq.ZArith.ZArith`` instead of ``Require Import ZArith``).
+
+ - Use the ``Locate`` command to find the fully-qualified name!
+
+- ``Require Import``’s should go in the following order:
+
+ 1. Standard library dependencies (start with ``Coq.``)
+
+ 2. External dependencies (anything outside the current project)
+
+ 3. Same-project dependencies
+
+- ``Require Import``’s with the same root library (the name before the first ``.``) should be
+ grouped together. Within each root-library group, they should be in alphabetical order (so
+ ``Coq.Lists.List`` before ``Coq.ZArith.ZArith``).
+
+.. _notations-and-scopes:
+
+Notations and scopes
+^^^^^^^^^^^^^^^^^^^^
+
+- Any file-wide ``Local Open Scope``’s should come immediately after the =Import=s (see example).
+
+ - Always use ``Local Open Scope``; just ``Open Scope`` will sneakily open the scope for those who
+ import your file.
+
+- Put notations in their own separate modules or files, so that those who import your file can
+ choose whether or not they want the notations.
+
+ - Conflicting notations can cause a lot of headache, so it comes in very handy to leave this
+ flexibility!
+
+.. _formatting:
+
+Formatting
+~~~~~~~~~~
+
+.. _line-length:
+
+Line length
+^^^^^^^^^^^
+
+- Maximum line length 80 characters.
+
+ - Many Coq IDE setups divide the screen in half vertically and use only half to display source
+ code, so more than 80 characters can be genuinely hard to read on a laptop.
+
+.. _whitespace-and-indentation:
+
+Whitespace and indentation
+^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+- No trailing whitespace.
+
+- Spaces, not tabs.
+
+- Files should end with a newline.
+
+ - Many editors do this automatically on save.
+
+- Colons may be either “English-spaced”, with no space before the colon and one space after (``x:
+ nat``) or “French-spaced”, with one space before and after (``x : nat``).
+
+- Default indentation is 2 spaces.
+
+ - Keeping this small prevents complex proofs from being indented ridiculously far, and matches IDE
+ defaults.
+
+- Use 2-space indents if inserting a line break immediately after:
+
+ - ``Proof.``
+
+ - ``fun <...> =>``
+
+ - ``forall <...>,``
+
+ - ``exists <....>,``
+
+- The style for indenting arguments in function application depends on where you make a line
+ break. If you make the line break immediately after the function name, use a 2-space
+ indent. However, if you make it after one or more arguments, align the next line with the first
+ argument:
+
+ .. code:: coq
+
+ (Z.pow
+ 1 2)
+ (Z.pow 1 2 3
+ 4 5 6)
+
+- ``Inductive`` cases should not be indented. Example:
+
+ .. code:: coq
+
+ Inductive Foo : Type :=
+ | FooA : Foo
+ | FooB : Foo
+ .
+
+- ``match`` or ``lazymatch`` cases should line up with the “m” in ``match`` or “l” in ``lazymatch``,
+ as in the following examples:
+
+ .. code:: coq
+
+ match x with
+ | 3 => true
+ | _ => false
+ end.
+
+ lazymatch x with
+ | 3 => idtac
+ | _ => fail "Not equal to 3:" x
+ end.
+
+ repeat match goal with
+ | _ => progress subst
+ | _ => reflexivity
+ end.
+
+ do 2 lazymatch goal with
+ | |- context [eq] => idtac
+ end.
+
+.. _definitions-and-fixpoints:
+
+Definitions and Fixpoints
+~~~~~~~~~~~~~~~~~~~~~~~~~
+
+- It’s okay to leave the return type of ``Definition``’s and ``Fixpoint``’s implicit
+ (e.g. ``Definition x := 5`` instead of ``Definition x : nat := 5``) when the type is very simple
+ or obvious (for instance, the definition is in a file which deals exclusively with operations on
+ ``Z``).
+
+.. _inductives:
+
+Inductives
+~~~~~~~~~~
+
+- The ``.`` ending an ``Inductive`` can be either on the same line as the last case or on its own
+ line immediately below. That is, both of the following are acceptable:
+
+ .. code:: coq
+
+ Inductive Foo : Type :=
+ | FooA : Foo
+ | FooB : Foo
+ .
+ Inductive Foo : Type :=
+ | FooA : Foo
+ | FooB : Foo.
+
+.. _lemmatheorem-statements:
+
+Lemma/Theorem statements
+~~~~~~~~~~~~~~~~~~~~~~~~
+
+- Generally, use ``Theorem`` for the most important, top-level facts you prove and ``Lemma`` for
+ everything else.
+
+- Insert a line break after the colon in the lemma statement.
+
+- Insert a line break after the comma for ``forall`` or ``exist`` quantifiers.
+
+- Implication arrows (``->``) should share a line with the previous hypothesis, not the following
+ one.
+
+- There is no need to make a line break after every ``->``; short preconditions may share a line.
+
+.. _proofs-and-tactics:
+
+Proofs and tactics
+~~~~~~~~~~~~~~~~~~
+
+- Use the ``Proof`` command (lined up vertically with ``Lemma`` or ``Theorem`` it corresponds to) to
+ open a proof, and indent the first line after it 2 spaces.
+
+- Very small proofs (where ``Proof. <tactics> Qed.`` is <= 80 characters) can go all in one line.
+
+- When ending a proof, align the ending statement (``Qed``, ``Admitted``, etc.) with ``Proof``.
+
+- Avoid referring to autogenerated names (e.g. ``H0``, ``n0``). It’s okay to let Coq generate these
+ names, but you should not explicitly refer to them in your proof. So ``intros; my_solver`` is
+ fine, but ``intros; apply H1; my_solver`` is not fine.
+
+ - You can force a non-autogenerated name by either putting the variable before the colon in the
+ lemma statement (``Lemma foo x : ...`` instead of ``Lemma foo : forall x, ...``), or by passing
+ arguments to ``intros`` (e.g. ``intros ? x`` to name the second argument ``x``)
+
+- This way, the proof won’t break when new hypotheses are added or autogenerated variable names
+ change.
+
+- Use curly braces ``{}`` for subgoals, instead of bullets.
+
+- *Never write tactics with more than one subgoal focused.* This can make the proof very confusing
+ to step through! If you have more than one subgoal, use curly braces.
+
+- Consider adding a comment after the opening curly brace that explains what case you’re in (see
+ example).
+
+ - This is not necessary for small subgoals but can help show the major lines of reasoning in large
+ proofs.
+
+- If invoking a tactic that is expected to return multiple subgoals, use ``[ | ... | ]`` before the
+ ``.`` to explicitly specify how many subgoals you expect.
+
+ - Examples: ``split; [ | ].`` ``induction z; [ | | ].``
+
+ - This helps make code more maintainable, because it fails immediately if your tactic no longer
+ solves as many subgoals as expected (or unexpectedly solves more).
+
+- If invoking a string of tactics (composed by ``;``) that will break the goal into multiple
+ subgoals and then solve all but one, still use ``[ ]`` to enforce that all but one goal is solved.
+
+ - Example: ``split; try lia; [ ]``.
+
+- Tactics that consist only of ``repeat``-ing a procedure (e.g. ``repeat match``, ``repeat first``)
+ should factor out a single step of that procedure a separate tactic called ``<tactic name>_step``,
+ because the single-step version is much easier to debug. For instance:
+
+ .. code:: coq
+
+ Ltac crush_step :=
+ match goal with
+ | _ => progress subst
+ | _ => reflexivity
+ end.
+ Ltac crush := repeat crush_step.
+
+.. _naming:
+
+Naming
+~~~~~~
+
+- Helper proofs about standard library datatypes should go in a module that is named to match the
+ standard library module (see example).
+
+ - This makes the helper proofs look like standard-library ones, which is helpful for categorizing
+ them if they’re genuinely at the standard-library level of abstraction.
+
+- Names of modules should start with capital letters.
+
+- Names of inductives and their constructors should start with capital letters.
+
+- Names of other definitions/lemmas should be snake case.
+
+.. _example:
+
+Example
+~~~~~~~
+
+A small standalone Coq file that exhibits many of the style points.
+
+.. code:: coq
+
+ (*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2021 Name <email@example.com>
+ *
+ * <License...>
+ *)
+
+ Require Import Coq.Lists.List.
+ Require Import Coq.micromega.Lia.
+ Require Import Coq.ZArith.ZArith.
+ Import ListNotations.
+ Local Open Scope Z_scope.
+
+ (* Helper proofs about standard library integers (Z) go within [Module Z] so
+ that they match standard-library Z lemmas when used. *)
+ Module Z.
+ Lemma pow_3_r x : x ^ 3 = x * x * x.
+ Proof. lia. Qed. (* very short proofs can go all on one line *)
+
+ Lemma pow_4_r x : x ^ 4 = x * x * x * x.
+ Proof.
+ change 4 with (Z.succ (Z.succ (Z.succ (Z.succ 0)))).
+ repeat match goal with
+ | _ => rewrite Z.pow_1_r
+ | _ => rewrite Z.pow_succ_r by lia
+ | |- context [x * (?a * ?b)] =>
+ replace (x * (a * b)) with (a * b * x) by lia
+ | _ => reflexivity
+ end.
+ Qed.
+ End Z.
+ (* Now we can access the lemmas above as Z.pow_3_r and Z.pow_4_r, as if they
+ were in the ZArith library! *)
+
+ Definition bar (x y : Z) := x ^ (y + 1).
+
+ (* example with a painfully manual proof to show case formatting *)
+ Lemma bar_upper_bound :
+ forall x y a,
+ 0 <= x <= a -> 0 <= y ->
+ 0 <= bar x y <= a ^ (y + 1).
+ Proof.
+ (* avoid referencing autogenerated names by explicitly naming variables *)
+ intros x y a Hx Hy. revert y Hy x a Hx.
+ (* explicitly indicate # subgoals with [ | ... | ] if > 1 *)
+ cbv [bar]; refine (natlike_ind _ _ _); [ | ].
+ { (* y = 0 *)
+ intros; lia. }
+ { (* y = Z.succ _ *)
+ intros.
+ rewrite Z.add_succ_l, Z.pow_succ_r by lia.
+ split.
+ { (* 0 <= bar x y *)
+ apply Z.mul_nonneg_nonneg; [ lia | ].
+ apply Z.pow_nonneg; lia. }
+ { (* bar x y < a ^ y *)
+ rewrite Z.pow_succ_r by lia.
+ apply Z.mul_le_mono_nonneg; try lia;
+ [ apply Z.pow_nonneg; lia | ].
+ (* For more flexible proofs, use match statements to find hypotheses
+ rather than referring to them by autogenerated names like H0. In this
+ case, we'll take any hypothesis that applies to and then solves the
+ goal. *)
+ match goal with H : _ |- _ => apply H; solve [auto] end. } }
+ Qed.
+
+ (* Put notations in a separate module or file so that importers can
+ decide whether or not to use them. *)
+ Module BarNotations.
+ Infix "#" := bar (at level 40) : Z_scope.
+ Notation "x '##'" := (bar x x) (at level 40) : Z_scope.
+ End BarNotations.
generated by cgit (git 2.34.1) at 2024-05-19 03:19:19 +0000