diff options
| author | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-09-19 00:54:08 +0000 |
|---|---|---|
| committer | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-09-19 00:54:08 +0000 |
| commit | a6fdaf10c24b5b01921b34b1d2cfc9ef3c23d50d (patch) | |
| tree | 52ad54ef5468d7755357dd0a2d513af94c3ea9b5 | |
| parent | 20a623794340113684dfeb5a7ff2e78f6a4d35f3 (diff) | |
| download | vericert-docs-a6fdaf10c24b5b01921b34b1d2cfc9ef3c23d50d.tar.gz vericert-docs-a6fdaf10c24b5b01921b34b1d2cfc9ef3c23d50d.zip | |
deploy: 8d74fffc72abb3cc20df691d9d40c73fbd1c0c27
| -rw-r--r-- | coq-style-guide/index.html | 115 | ||||
| -rw-r--r-- | docs/building/index.html | 25 | ||||
| -rw-r--r-- | docs/index.html | 5 | ||||
| -rw-r--r-- | docs/unreleased/index.html | 5 | ||||
| -rw-r--r-- | docs/using-vericert/index.html | 21 | ||||
| -rw-r--r-- | future/index.html | 3 | ||||
| -rw-r--r-- | index.html | 8 |
7 files changed, 96 insertions, 86 deletions
diff --git a/coq-style-guide/index.html b/coq-style-guide/index.html index 1e64037..f3a3dc5 100644 --- a/coq-style-guide/index.html +++ b/coq-style-guide/index.html @@ -3,35 +3,31 @@ Code organization # Legal banner # Files should begin with a copyright/licens Code organization # Legal banner # Files should begin with a copyright/license banner, as shown in the example above."><meta property="og:type" content="article"><meta property="og:url" content="https://vericert.ymhg.org/coq-style-guide/"><title>Coq Style Guide |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.09c4470fdacb71a68922c07311d906b9cd808586067883b11db52f10e30e96d4.js integrity="sha256-CcRHD9rLcaaJIsBzEdkGuc2AhYYGeIOxHbUvEOMOltQ="></script></head><body><input type=checkbox class="hidden toggle" id=menu-control> <input type=checkbox class="hidden toggle" id=toc-control><main class="container flex"><aside class=book-menu><nav><div class=book-brand><a href=/><div id=book-logo></div><span></span></a><p>A formally verified high-level synthesis tool written in Coq.</p></div><div class=book-search><input type=text id=book-search-input placeholder=Search aria-label=Search maxlength=64 data-hotkeys=s/><div class="book-search-spinner hidden"></div><ul id=book-search-results></ul></div><ul><li><a href=https://vericert.ymhg.org/coq-style-guide/ class=active>Coq Style Guide</a></li><li><a href=https://vericert.ymhg.org/docs/>Docs</a><ul><li><a href=https://vericert.ymhg.org/docs/building/>Building Vericert</a></li><li><a href=https://vericert.ymhg.org/docs/unreleased/>Unreleased Features</a></li><li><a href=https://vericert.ymhg.org/docs/using-vericert/>Using Vericert</a></li></ul></li><li><a href=https://vericert.ymhg.org/future/>Future Work</a></li></ul><ul><li><a href=https://github.com/ymherklotz/vericert target=_blank rel=noopener>Github</a></li></ul></nav><script>(function(){var menu=document.querySelector("aside.book-menu nav");addEventListener("beforeunload",function(event){localStorage.setItem("menu.scrollTop",menu.scrollTop);});menu.scrollTop=localStorage.getItem("menu.scrollTop");})();</script></aside><div class=book-page><header class=book-header><div class="flex align-center justify-between"><label for=menu-control><img src=/svg/menu.svg class=book-icon alt=Menu></label> <strong>Coq Style Guide</strong> -<label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents><ul><li><ul><li><a href=#code-organization>Code organization</a><ul><li><a href=#legal-banner>Legal banner</a></li><li><a href=#import-statements>Import statements</a></li><li><a href=#notations-and-scopes>Notations and scopes</a></li></ul></li><li><a href=#formatting>Formatting</a><ul><li><a href=#line-length>Line length</a></li><li><a href=#whitespace-and-indentation>Whitespace and indentation</a></li></ul></li><li><a href=#definitions-and-fixpoints>Definitions and Fixpoints</a></li><li><a href=#inductives>Inductives</a></li><li><a href=#lemmatheorem-statements>Lemma/Theorem statements</a></li><li><a href=#proofs-and-tactics>Proofs and tactics</a></li><li><a href=#naming>Naming</a></li><li><a href=#example>Example</a></li></ul></li></ul></nav></aside></header><h1>Coq Style Guide</h1><article class=markdown><p>This style guide was taken from <a href=https://github.com/project-oak/silveroak>Silveroak</a>, 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 <a href=#example>example</a> at the bottom of this file.</p><h2 id=code-organization>Code organization +<label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents><ul><li><ul><li><a href=#code-organization>Code organization</a><ul><li><a href=#legal-banner>Legal banner</a></li><li><a href=#import-statements>Import statements</a></li><li><a href=#notations-and-scopes>Notations and scopes</a></li></ul></li><li><a href=#formatting>Formatting</a><ul><li><a href=#line-length>Line length</a></li><li><a href=#whitespace-and-indentation>Whitespace and indentation</a></li></ul></li><li><a href=#definitions-and-fixpoints>Definitions and Fixpoints</a></li><li><a href=#inductives>Inductives</a></li><li><a href=#lemmatheorem-statements>Lemma/Theorem statements</a></li><li><a href=#proofs-and-tactics>Proofs and tactics</a></li><li><a href=#naming>Naming</a></li><li><a href=#example>Example</a></li></ul></li></ul></nav></aside></header><h1>Coq Style Guide</h1><article class=markdown><p>This style guide was taken from <a href=https://github.com/project-oak/silveroak>Silveroak</a>, 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 <a href=#example>example</a> at the +bottom of this file.</p><h2 id=code-organization>Code organization <a class=anchor href=#code-organization>#</a></h2><h3 id=legal-banner>Legal banner -<a class=anchor href=#legal-banner>#</a></h3><ul><li>Files should begin with a copyright/license banner, as shown in the example -above.</li></ul><h3 id=import-statements>Import statements -<a class=anchor href=#import-statements>#</a></h3><ul><li><p><code>Require Import</code> statements should all go at the top of the file, followed by -file-wide <code>Import</code> statements.</p><ul><li>=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.</li></ul></li><li><p>One <code>Require Import</code> statement per line; it’s easier to scan that way.</p></li><li><p><code>Require Import</code> statements should use “fully-qualified” names (e.g. =Require -Import Coq.ZArith.ZArith= instead of <code>Require Import ZArith</code>).</p><ul><li>Use the <code>Locate</code> command to find the fully-qualified name!</li></ul></li><li><p><code>Require Import</code>’s should go in the following order:</p><ol><li>Standard library dependencies (start with <code>Coq.</code>)</li><li>External dependencies (anything outside the current project)</li><li>Same-project dependencies</li></ol></li><li><p><code>Require Import</code>’s with the same root library (the name before the first <code>.</code>) -should be grouped together. Within each root-library group, they should be in -alphabetical order (so <code>Coq.Lists.List</code> before <code>Coq.ZArith.ZArith</code>).</p></li></ul><h3 id=notations-and-scopes>Notations and scopes -<a class=anchor href=#notations-and-scopes>#</a></h3><ul><li><p>Any file-wide <code>Local Open Scope</code>’s should come immediately after the =Import=s -(see example).</p><ul><li>Always use <code>Local Open Scope</code>; just <code>Open Scope</code> will sneakily open the scope -for those who import your file.</li></ul></li><li><p>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.</p><ul><li>Conflicting notations can cause a lot of headache, so it comes in very handy -to leave this flexibility!</li></ul></li></ul><h2 id=formatting>Formatting +<a class=anchor href=#legal-banner>#</a></h3><ul><li>Files should begin with a copyright/license banner, as shown in the example above.</li></ul><h3 id=import-statements>Import statements +<a class=anchor href=#import-statements>#</a></h3><ul><li><p><code>Require Import</code> statements should all go at the top of the file, followed by file-wide <code>Import</code> +statements.</p><ul><li>=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.</li></ul></li><li><p>One <code>Require Import</code> statement per line; it’s easier to scan that way.</p></li><li><p><code>Require Import</code> statements should use “fully-qualified” names (e.g. =Require Import +Coq.ZArith.ZArith= instead of <code>Require Import ZArith</code>).</p><ul><li>Use the <code>Locate</code> command to find the fully-qualified name!</li></ul></li><li><p><code>Require Import</code>’s should go in the following order:</p><ol><li>Standard library dependencies (start with <code>Coq.</code>)</li><li>External dependencies (anything outside the current project)</li><li>Same-project dependencies</li></ol></li><li><p><code>Require Import</code>’s with the same root library (the name before the first <code>.</code>) should be grouped +together. Within each root-library group, they should be in alphabetical order (so <code>Coq.Lists.List</code> +before <code>Coq.ZArith.ZArith</code>).</p></li></ul><h3 id=notations-and-scopes>Notations and scopes +<a class=anchor href=#notations-and-scopes>#</a></h3><ul><li><p>Any file-wide <code>Local Open Scope</code>’s should come immediately after the =Import=s (see example).</p><ul><li>Always use <code>Local Open Scope</code>; just <code>Open Scope</code> will sneakily open the scope for those who import +your file.</li></ul></li><li><p>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.</p><ul><li>Conflicting notations can cause a lot of headache, so it comes in very handy to leave this +flexibility!</li></ul></li></ul><h2 id=formatting>Formatting <a class=anchor href=#formatting>#</a></h2><h3 id=line-length>Line length -<a class=anchor href=#line-length>#</a></h3><ul><li>Maximum line length 80 characters.<ul><li>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.</li></ul></li></ul><h3 id=whitespace-and-indentation>Whitespace and indentation -<a class=anchor href=#whitespace-and-indentation>#</a></h3><ul><li><p>No trailing whitespace.</p></li><li><p>Spaces, not tabs.</p></li><li><p>Files should end with a newline.</p><ul><li>Many editors do this automatically on save.</li></ul></li><li><p>Colons may be either “English-spaced”, with no space before the colon and one -space after (<code>x: nat</code>) or “French-spaced”, with one space before and after (<code>x : nat</code>).</p></li><li><p>Default indentation is 2 spaces.</p><ul><li>Keeping this small prevents complex proofs from being indented ridiculously -far, and matches IDE defaults.</li></ul></li><li><p>Use 2-space indents if inserting a line break immediately after:</p><ul><li><code>Proof.</code></li><li><code>fun <...> =></code></li><li><code>forall <...>,</code></li><li><code>exists <....>,</code></li></ul></li><li><p>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:</p><div class=highlight><pre class=chroma><code class=language-coq data-lang=coq><span class=o>(</span><span class=n>Z</span><span class=o>.</span><span class=n>pow</span> +<a class=anchor href=#line-length>#</a></h3><ul><li>Maximum line length 80 characters.<ul><li>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.</li></ul></li></ul><h3 id=whitespace-and-indentation>Whitespace and indentation +<a class=anchor href=#whitespace-and-indentation>#</a></h3><ul><li><p>No trailing whitespace.</p></li><li><p>Spaces, not tabs.</p></li><li><p>Files should end with a newline.</p><ul><li>Many editors do this automatically on save.</li></ul></li><li><p>Colons may be either “English-spaced”, with no space before the colon and one space after (<code>x: nat</code>) +or “French-spaced”, with one space before and after (<code>x : nat</code>).</p></li><li><p>Default indentation is 2 spaces.</p><ul><li>Keeping this small prevents complex proofs from being indented ridiculously far, and matches IDE +defaults.</li></ul></li><li><p>Use 2-space indents if inserting a line break immediately after:</p><ul><li><code>Proof.</code></li><li><code>fun <...> =></code></li><li><code>forall <...>,</code></li><li><code>exists <....>,</code></li></ul></li><li><p>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:</p><div class=highlight><pre class=chroma><code class=language-coq data-lang=coq><span class=o>(</span><span class=n>Z</span><span class=o>.</span><span class=n>pow</span> <span class=n>1</span> <span class=n>2</span><span class=o>)</span> <span class=o>(</span><span class=n>Z</span><span class=o>.</span><span class=n>pow</span> <span class=n>1</span> <span class=n>2</span> <span class=n>3</span> <span class=n>4</span> <span class=n>5</span> <span class=n>6</span><span class=o>)</span> @@ -39,8 +35,8 @@ arguments, align the next line with the first argument:</p><div class=highlight> <span class=o>|</span> <span class=n>FooA</span> <span class=o>:</span> <span class=n>Foo</span> <span class=o>|</span> <span class=n>FooB</span> <span class=o>:</span> <span class=n>Foo</span> <span class=o>.</span> -</code></pre></div></li><li><p><code>match</code> or <code>lazymatch</code> cases should line up with the “m” in <code>match</code> or “l” in -<code>lazymatch</code>, as in the following examples:</p><div class=highlight><pre class=chroma><code class=language-coq data-lang=coq><span class=k>match</span> <span class=n>x</span> <span class=k>with</span> +</code></pre></div></li><li><p><code>match</code> or <code>lazymatch</code> cases should line up with the “m” in <code>match</code> or “l” in <code>lazymatch</code>, as in the +following examples:</p><div class=highlight><pre class=chroma><code class=language-coq data-lang=coq><span class=k>match</span> <span class=n>x</span> <span class=k>with</span> <span class=o>|</span> <span class=n>3</span> <span class=o>=></span> <span class=bp>true</span> <span class=o>|</span> <span class=o>_</span> <span class=o>=></span> <span class=bp>false</span> <span class=k>end</span><span class=o>.</span> @@ -59,13 +55,11 @@ arguments, align the next line with the first argument:</p><div class=highlight> <span class=o>|</span> <span class=o>|-</span> <span class=n>context</span> <span class=o>[</span><span class=n>eq</span><span class=o>]</span> <span class=o>=></span> <span class=kr>idtac</span> <span class=k>end</span><span class=o>.</span> </code></pre></div></li></ul><h2 id=definitions-and-fixpoints>Definitions and Fixpoints -<a class=anchor href=#definitions-and-fixpoints>#</a></h2><ul><li>It’s okay to leave the return type of <code>Definition</code>’s and <code>Fixpoint</code>’s implicit -(e.g. <code>Definition x := 5</code> instead of <code>Definition x : nat := 5</code>) when the type is -very simple or obvious (for instance, the definition is in a file which deals -exclusively with operations on <code>Z</code>).</li></ul><h2 id=inductives>Inductives -<a class=anchor href=#inductives>#</a></h2><ul><li><p>The <code>.</code> ending an <code>Inductive</code> 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:</p><div class=highlight><pre class=chroma><code class=language-coq data-lang=coq><span class=kn>Inductive</span> <span class=n>Foo</span> <span class=o>:</span> <span class=kt>Type</span> <span class=o>:=</span> +<a class=anchor href=#definitions-and-fixpoints>#</a></h2><ul><li>It’s okay to leave the return type of <code>Definition</code>’s and <code>Fixpoint</code>’s implicit (e.g. <code>Definition x := 5</code> +instead of <code>Definition x : nat := 5</code>) when the type is very simple or obvious (for instance, the +definition is in a file which deals exclusively with operations on <code>Z</code>).</li></ul><h2 id=inductives>Inductives +<a class=anchor href=#inductives>#</a></h2><ul><li><p>The <code>.</code> ending an <code>Inductive</code> 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:</p><div class=highlight><pre class=chroma><code class=language-coq data-lang=coq><span class=kn>Inductive</span> <span class=n>Foo</span> <span class=o>:</span> <span class=kt>Type</span> <span class=o>:=</span> <span class=o>|</span> <span class=n>FooA</span> <span class=o>:</span> <span class=n>Foo</span> <span class=o>|</span> <span class=n>FooB</span> <span class=o>:</span> <span class=n>Foo</span> <span class=o>.</span> @@ -73,41 +67,32 @@ acceptable:</p><div class=highlight><pre class=chroma><code class=language-coq d <span class=o>|</span> <span class=n>FooA</span> <span class=o>:</span> <span class=n>Foo</span> <span class=o>|</span> <span class=n>FooB</span> <span class=o>:</span> <span class=n>Foo</span><span class=o>.</span> </code></pre></div></li></ul><h2 id=lemmatheorem-statements>Lemma/Theorem statements -<a class=anchor href=#lemmatheorem-statements>#</a></h2><ul><li>Generally, use <code>Theorem</code> for the most important, top-level facts you prove and -<code>Lemma</code> for everything else.</li><li>Insert a line break after the colon in the lemma statement.</li><li>Insert a line break after the comma for <code>forall</code> or <code>exist</code> quantifiers.</li><li>Implication arrows (<code>-></code>) should share a line with the previous hypothesis, not -the following one.</li><li>There is no need to make a line break after every <code>-></code>; short preconditions may -share a line.</li></ul><h2 id=proofs-and-tactics>Proofs and tactics -<a class=anchor href=#proofs-and-tactics>#</a></h2><ul><li><p>Use the <code>Proof</code> command (lined up vertically with <code>Lemma</code> or <code>Theorem</code> it -corresponds to) to open a proof, and indent the first line after it 2 spaces.</p></li><li><p>Very small proofs (where <code>Proof. <tactics> Qed.</code> is <= 80 characters) can go all -in one line.</p></li><li><p>When ending a proof, align the ending statement (<code>Qed</code>, <code>Admitted</code>, etc.) with -<code>Proof</code>.</p></li><li><p>Avoid referring to autogenerated names (e.g. =H0=, <code>n0</code>). It’s okay to let Coq -generate these names, but you should not explicitly refer to them in your -proof. So <code>intros; my_solver</code> is fine, but <code>intros; apply H1; my_solver</code> is not -fine.</p><ul><li>You can force a non-autogenerated name by either putting the variable before -the colon in the lemma statement (<code>Lemma foo x : ...</code> instead of <code>Lemma foo : forall x, ...</code>), or by passing arguments to <code>intros</code> (e.g. =intros ? x= to name -the second argument <code>x</code>)</li></ul></li><li><p>This way, the proof won’t break when new hypotheses are added or autogenerated -variable names change.</p></li><li><p>Use curly braces <code>{}</code> for subgoals, instead of bullets.</p></li><li><p><em>Never write tactics with more than one subgoal focused.</em> This can make the -proof very confusing to step through! If you have more than one subgoal, use -curly braces.</p></li><li><p>Consider adding a comment after the opening curly brace that explains what -case you’re in (see example).</p><ul><li>This is not necessary for small subgoals but can help show the major lines -of reasoning in large proofs.</li></ul></li><li><p>If invoking a tactic that is expected to return multiple subgoals, use <code>[ | ... | ]</code> before the <code>.</code> to explicitly specify how many subgoals you expect.</p><ul><li>Examples: <code>split; [ | ].</code> <code>induction z; [ | | ].</code></li><li>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).</li></ul></li><li><p>If invoking a string of tactics (composed by <code>;</code>) that will break the goal into -multiple subgoals and then solve all but one, still use <code>[ ]</code> to enforce that -all but one goal is solved.</p><ul><li>Example: <code>split; try lia; [ ]</code>.</li></ul></li><li><p>Tactics that consist only of <code>repeat</code>-ing a procedure (e.g. <code>repeat match</code>, -<code>repeat first</code>) should factor out a single step of that procedure a separate -tactic called <code><tactic name>_step</code>, because the single-step version is much -easier to debug. For instance:</p><div class=highlight><pre class=chroma><code class=language-coq data-lang=coq><span class=kn>Ltac</span> <span class=n>crush_step</span> <span class=o>:=</span> +<a class=anchor href=#lemmatheorem-statements>#</a></h2><ul><li>Generally, use <code>Theorem</code> for the most important, top-level facts you prove and <code>Lemma</code> for everything +else.</li><li>Insert a line break after the colon in the lemma statement.</li><li>Insert a line break after the comma for <code>forall</code> or <code>exist</code> quantifiers.</li><li>Implication arrows (<code>-></code>) should share a line with the previous hypothesis, not the following one.</li><li>There is no need to make a line break after every <code>-></code>; short preconditions may share a line.</li></ul><h2 id=proofs-and-tactics>Proofs and tactics +<a class=anchor href=#proofs-and-tactics>#</a></h2><ul><li><p>Use the <code>Proof</code> command (lined up vertically with <code>Lemma</code> or <code>Theorem</code> it corresponds to) to open a +proof, and indent the first line after it 2 spaces.</p></li><li><p>Very small proofs (where <code>Proof. <tactics> Qed.</code> is <= 80 characters) can go all in one line.</p></li><li><p>When ending a proof, align the ending statement (<code>Qed</code>, <code>Admitted</code>, etc.) with <code>Proof</code>.</p></li><li><p>Avoid referring to autogenerated names (e.g. =H0=, <code>n0</code>). It’s okay to let Coq generate these names, +but you should not explicitly refer to them in your proof. So <code>intros; my_solver</code> is fine, but +<code>intros; apply H1; my_solver</code> is not fine.</p><ul><li>You can force a non-autogenerated name by either putting the variable before the colon in the +lemma statement (<code>Lemma foo x : ...</code> instead of <code>Lemma foo : forall x, ...</code>), or by passing +arguments to <code>intros</code> (e.g. =intros ? x= to name the second argument <code>x</code>)</li></ul></li><li><p>This way, the proof won’t break when new hypotheses are added or autogenerated variable names +change.</p></li><li><p>Use curly braces <code>{}</code> for subgoals, instead of bullets.</p></li><li><p><em>Never write tactics with more than one subgoal focused.</em> This can make the proof very confusing to +step through! If you have more than one subgoal, use curly braces.</p></li><li><p>Consider adding a comment after the opening curly brace that explains what case you’re in (see +example).</p><ul><li>This is not necessary for small subgoals but can help show the major lines of reasoning in large +proofs.</li></ul></li><li><p>If invoking a tactic that is expected to return multiple subgoals, use <code>[ | ... | ]</code> before the <code>.</code> to +explicitly specify how many subgoals you expect.</p><ul><li>Examples: <code>split; [ | ].</code> <code>induction z; [ | | ].</code></li><li>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).</li></ul></li><li><p>If invoking a string of tactics (composed by <code>;</code>) that will break the goal into multiple subgoals +and then solve all but one, still use <code>[ ]</code> to enforce that all but one goal is solved.</p><ul><li>Example: <code>split; try lia; [ ]</code>.</li></ul></li><li><p>Tactics that consist only of <code>repeat</code>-ing a procedure (e.g. <code>repeat match</code>, <code>repeat first</code>) should +factor out a single step of that procedure a separate tactic called <code><tactic name>_step</code>, because +the single-step version is much easier to debug. For instance:</p><div class=highlight><pre class=chroma><code class=language-coq data-lang=coq><span class=kn>Ltac</span> <span class=n>crush_step</span> <span class=o>:=</span> <span class=k>match</span> <span class=n>goal</span> <span class=k>with</span> <span class=o>|</span> <span class=o>_</span> <span class=o>=></span> <span class=n>progress</span> <span class=k>subst</span> <span class=o>|</span> <span class=o>_</span> <span class=o>=></span> <span class=kp>reflexivity</span> <span class=k>end</span><span class=o>.</span> <span class=kn>Ltac</span> <span class=n>crush</span> <span class=o>:=</span> <span class=kr>repeat</span> <span class=n>crush_step</span><span class=o>.</span> </code></pre></div></li></ul><h2 id=naming>Naming -<a class=anchor href=#naming>#</a></h2><ul><li><p>Helper proofs about standard library datatypes should go in a module that is -named to match the standard library module (see example).</p><ul><li>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.</li></ul></li><li><p>Names of modules should start with capital letters.</p></li><li><p>Names of inductives and their constructors should start with capital letters.</p></li><li><p>Names of other definitions/lemmas should be snake case.</p></li></ul><h2 id=example>Example +<a class=anchor href=#naming>#</a></h2><ul><li><p>Helper proofs about standard library datatypes should go in a module that is named to match the +standard library module (see example).</p><ul><li>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.</li></ul></li><li><p>Names of modules should start with capital letters.</p></li><li><p>Names of inductives and their constructors should start with capital letters.</p></li><li><p>Names of other definitions/lemmas should be snake case.</p></li></ul><h2 id=example>Example <a class=anchor href=#example>#</a></h2><p>A small standalone Coq file that exhibits many of the style points.</p><div class=highlight><pre class=chroma><code class=language-coq data-lang=coq><span class=c>(* </span><span class=c> * Vericert: Verified high-level synthesis. </span><span class=c> * Copyright (C) 2021 Name <email@example.com> diff --git a/docs/building/index.html b/docs/building/index.html index c761f82..43ca1ba 100644 --- a/docs/building/index.html +++ b/docs/building/index.html @@ -5,16 +5,27 @@ The project is written in Coq, a theorem prover, which is extracted to OCaml so Coq: theorem prover that is used to also program the HLS tool."><meta property="og:type" content="article"><meta property="og:url" content="https://vericert.ymhg.org/docs/building/"><title>Building Vericert |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.09c4470fdacb71a68922c07311d906b9cd808586067883b11db52f10e30e96d4.js integrity="sha256-CcRHD9rLcaaJIsBzEdkGuc2AhYYGeIOxHbUvEOMOltQ="></script></head><body><input type=checkbox class="hidden toggle" id=menu-control> <input type=checkbox class="hidden toggle" id=toc-control><main class="container flex"><aside class=book-menu><nav><div class=book-brand><a href=/><div id=book-logo></div><span></span></a><p>A formally verified high-level synthesis tool written in Coq.</p></div><div class=book-search><input type=text id=book-search-input placeholder=Search aria-label=Search maxlength=64 data-hotkeys=s/><div class="book-search-spinner hidden"></div><ul id=book-search-results></ul></div><ul><li><a href=https://vericert.ymhg.org/coq-style-guide/>Coq Style Guide</a></li><li><a href=https://vericert.ymhg.org/docs/>Docs</a><ul><li><a href=https://vericert.ymhg.org/docs/building/ class=active>Building Vericert</a></li><li><a href=https://vericert.ymhg.org/docs/unreleased/>Unreleased Features</a></li><li><a href=https://vericert.ymhg.org/docs/using-vericert/>Using Vericert</a></li></ul></li><li><a href=https://vericert.ymhg.org/future/>Future Work</a></li></ul><ul><li><a href=https://github.com/ymherklotz/vericert target=_blank rel=noopener>Github</a></li></ul></nav><script>(function(){var menu=document.querySelector("aside.book-menu nav");addEventListener("beforeunload",function(event){localStorage.setItem("menu.scrollTop",menu.scrollTop);});menu.scrollTop=localStorage.getItem("menu.scrollTop");})();</script></aside><div class=book-page><header class=book-header><div class="flex align-center justify-between"><label for=menu-control><img src=/svg/menu.svg class=book-icon alt=Menu></label> <strong>Building Vericert</strong> -<label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents><ul><li><ul><li><a href=#downloading-compcert>Downloading CompCert</a></li><li><a href=#setting-up-nix>Setting up Nix</a></li><li><a href=#makefile-build>Makefile build</a></li><li><a href=#testing>Testing</a></li></ul></li></ul></nav></aside></header><h1>Building Vericert</h1><article class=markdown><p>To build Vericert, the provided Makefile can be used. External dependencies are needed to build the project, which can be pulled in automatically with <a href=https://nixos.org/nix/>nix</a> using the provided <code>default.nix</code> and <code>shell.nix</code> files.</p><p>The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following:</p><ul><li><a href=https://coq.inria.fr/>Coq</a>: theorem prover that is used to also program the HLS tool.</li><li><a href=https://ocaml.org/>OCaml</a>: the OCaml compiler to compile the extracted files.</li><li><a href=https://github.com/mit-plv/bbv>bbv</a>: an efficient bit vector library.</li><li><a href=https://github.com/ocaml/dune>dune</a>: build tool for ocaml projects to gather all the ocaml files and compile them in the right order.</li><li><a href=http://gallium.inria.fr/~fpottier/menhir/>menhir</a>: parser generator for ocaml.</li><li><a href=https://github.com/ocaml/ocamlfind>findlib</a> to find installed OCaml libraries.</li><li><a href=https://gcc.gnu.org/>GCC</a>: compiler to help build CompCert.</li></ul><p>These dependencies can be installed manually, or automatically through Nix.</p><h2 id=downloading-compcert>Downloading CompCert -<a class=anchor href=#downloading-compcert>#</a></h2><p>CompCert is added as a submodule in the <code>lib/CompCert</code> directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, you can run:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>git clone --recursive https://github.com/ymherklotz/vericert -</code></pre></div><p>If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>git submodule update --init +<label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents><ul><li><ul><li><a href=#downloading-compcert>Downloading CompCert</a></li><li><a href=#setting-up-nix>Setting up Nix</a></li><li><a href=#makefile-build>Makefile build</a></li><li><a href=#testing>Testing</a></li></ul></li></ul></nav></aside></header><h1>Building Vericert</h1><article class=markdown><p>To build Vericert, the provided Makefile can be used. External dependencies are needed to build the +project, which can be pulled in automatically with <a href=https://nixos.org/nix/>nix</a> using the provided <code>default.nix</code> and <code>shell.nix</code> +files.</p><p>The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be +compiled and executed. The dependencies of this project are the following:</p><ul><li><a href=https://coq.inria.fr/>Coq</a>: theorem prover that is used to also program the HLS tool.</li><li><a href=https://ocaml.org/>OCaml</a>: the OCaml compiler to compile the extracted files.</li><li><a href=https://github.com/mit-plv/bbv>bbv</a>: an efficient bit vector library.</li><li><a href=https://github.com/ocaml/dune>dune</a>: build tool for ocaml projects to gather all the ocaml files and compile them in the right +order.</li><li><a href=http://gallium.inria.fr/~fpottier/menhir/>menhir</a>: parser generator for ocaml.</li><li><a href=https://github.com/ocaml/ocamlfind>findlib</a> to find installed OCaml libraries.</li><li><a href=https://gcc.gnu.org/>GCC</a>: compiler to help build CompCert.</li></ul><p>These dependencies can be installed manually, or automatically through Nix.</p><h2 id=downloading-compcert>Downloading CompCert +<a class=anchor href=#downloading-compcert>#</a></h2><p>CompCert is added as a submodule in the <code>lib/CompCert</code> directory. It is needed to run the build +process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded +together with the repository. To clone CompCert together with this project, you can run:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>git clone --recursive https://github.com/ymherklotz/vericert +</code></pre></div><p>If the repository is already cloned, you can run the following command to make sure that CompCert is +also downloaded:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>git submodule update --init </code></pre></div><h2 id=setting-up-nix>Setting up Nix -<a class=anchor href=#setting-up-nix>#</a></h2><p>Nix is a package manager that can create an isolated environment so that the builds are reproducible. Once nix is installed, it can be used in the following way.</p><p>To open a shell which includes all the necessary dependencies, one can use:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>nix-shell +<a class=anchor href=#setting-up-nix>#</a></h2><p>Nix is a package manager that can create an isolated environment so that the builds are +reproducible. Once nix is installed, it can be used in the following way.</p><p>To open a shell which includes all the necessary dependencies, one can use:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>nix-shell </code></pre></div><p>which will open a shell that has all the dependencies loaded.</p><h2 id=makefile-build>Makefile build -<a class=anchor href=#makefile-build>#</a></h2><p>If the dependencies were installed manually, or if one is in the <code>nix-shell</code>, the project can be built by running:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>make -j8 +<a class=anchor href=#makefile-build>#</a></h2><p>If the dependencies were installed manually, or if one is in the <code>nix-shell</code>, the project can be built +by running:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>make -j8 </code></pre></div><p>and installed locally, or under the <code>PREFIX</code> location using:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>make install -</code></pre></div><p>Which will install the binary in <code>./bin/vericert</code> by default. However, this can be changed by changing the <code>PREFIX</code> environment variable, in which case the binary will be installed in <code>$PREFIX/bin/vericert</code>.</p><h2 id=testing>Testing -<a class=anchor href=#testing>#</a></h2><p>To test out <code>vericert</code> you can try the following examples which are in the test folder using the following:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>./bin/vericert test/loop.c -o loop.v +</code></pre></div><p>Which will install the binary in <code>./bin/vericert</code> by default. However, this can be changed by changing +the <code>PREFIX</code> environment variable, in which case the binary will be installed in <code>$PREFIX/bin/vericert</code>.</p><h2 id=testing>Testing +<a class=anchor href=#testing>#</a></h2><p>To test out <code>vericert</code> you can try the following examples which are in the test folder using the +following:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=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 </code></pre></div><p>Or by running the test suite using the following command:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>make <span class=nb>test</span> diff --git a/docs/index.html b/docs/index.html index 5c47f44..6b9cf54 100644 --- a/docs/index.html +++ b/docs/index.html @@ -4,4 +4,7 @@ The design shown in Figure 1 shows how Vericert leverages an existing verified C compiler called CompCert to perform this translation."><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Docs"><meta property="og:description" content><meta property="og:type" content="website"><meta property="og:url" content="https://vericert.ymhg.org/docs/"><title>Docs |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.09c4470fdacb71a68922c07311d906b9cd808586067883b11db52f10e30e96d4.js integrity="sha256-CcRHD9rLcaaJIsBzEdkGuc2AhYYGeIOxHbUvEOMOltQ="></script><link rel=alternate type=application/rss+xml href=https://vericert.ymhg.org/docs/index.xml></head><body><input type=checkbox class="hidden toggle" id=menu-control> <input type=checkbox class="hidden toggle" id=toc-control><main class="container flex"><aside class=book-menu><nav><div class=book-brand><a href=/><div id=book-logo></div><span></span></a><p>A formally verified high-level synthesis tool written in Coq.</p></div><div class=book-search><input type=text id=book-search-input placeholder=Search aria-label=Search maxlength=64 data-hotkeys=s/><div class="book-search-spinner hidden"></div><ul id=book-search-results></ul></div><ul><li><a href=https://vericert.ymhg.org/coq-style-guide/>Coq Style Guide</a></li><li><a href=https://vericert.ymhg.org/docs/ class=active>Docs</a><ul><li><a href=https://vericert.ymhg.org/docs/building/>Building Vericert</a></li><li><a href=https://vericert.ymhg.org/docs/unreleased/>Unreleased Features</a></li><li><a href=https://vericert.ymhg.org/docs/using-vericert/>Using Vericert</a></li></ul></li><li><a href=https://vericert.ymhg.org/future/>Future Work</a></li></ul><ul><li><a href=https://github.com/ymherklotz/vericert target=_blank rel=noopener>Github</a></li></ul></nav><script>(function(){var menu=document.querySelector("aside.book-menu nav");addEventListener("beforeunload",function(event){localStorage.setItem("menu.scrollTop",menu.scrollTop);});menu.scrollTop=localStorage.getItem("menu.scrollTop");})();</script></aside><div class=book-page><header class=book-header><div class="flex align-center justify-between"><label for=menu-control><img src=/svg/menu.svg class=book-icon alt=Menu></label> <strong>Docs</strong> -<label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents></nav></aside></header><h1>Docs</h1><article class=markdown><p>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).</p><p><a id=org52e0c8a></a></p><figure><img src=/images/design.jpg alt="Figure 1: 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." width=600><figcaption><p>Figure 1: 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.</p></figcaption></figure><p>The design shown in Figure <a href=#org52e0c8a>1</a> shows how Vericert leverages an existing verified C compiler called <a href=https://compcert.org/compcert-C.html>CompCert</a> to perform this translation.</p></article><footer class=book-footer><div class="flex flex-wrap justify-between"></div></footer><div class=book-comments></div><label for=menu-control class="hidden book-menu-overlay"></label></div><aside class=book-toc><nav id=TableOfContents></nav></aside></main></body></html>
\ No newline at end of file +<label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents></nav></aside></header><h1>Docs</h1><article class=markdown><p>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).</p><p><a id=orgd5c959a></a></p><figure><img src=/images/design.jpg alt="Figure 1: 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." width=600><figcaption><p>Figure 1: 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.</p></figcaption></figure><p>The design shown in Figure <a href=#orgd5c959a>1</a> shows how Vericert leverages an existing verified C compiler +called <a href=https://compcert.org/compcert-C.html>CompCert</a> to perform this translation.</p></article><footer class=book-footer><div class="flex flex-wrap justify-between"></div></footer><div class=book-comments></div><label for=menu-control class="hidden book-menu-overlay"></label></div><aside class=book-toc><nav id=TableOfContents></nav></aside></main></body></html>
\ No newline at end of file diff --git a/docs/unreleased/index.html b/docs/unreleased/index.html index 1cf635a..489c576 100644 --- a/docs/unreleased/index.html +++ b/docs/unreleased/index.html @@ -3,7 +3,10 @@ scheduling, if-conversion, loop pipelining, 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."><meta property="og:type" content="article"><meta property="og:url" content="https://vericert.ymhg.org/docs/unreleased/"><title>Unreleased Features |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.09c4470fdacb71a68922c07311d906b9cd808586067883b11db52f10e30e96d4.js integrity="sha256-CcRHD9rLcaaJIsBzEdkGuc2AhYYGeIOxHbUvEOMOltQ="></script></head><body><input type=checkbox class="hidden toggle" id=menu-control> <input type=checkbox class="hidden toggle" id=toc-control><main class="container flex"><aside class=book-menu><nav><div class=book-brand><a href=/><div id=book-logo></div><span></span></a><p>A formally verified high-level synthesis tool written in Coq.</p></div><div class=book-search><input type=text id=book-search-input placeholder=Search aria-label=Search maxlength=64 data-hotkeys=s/><div class="book-search-spinner hidden"></div><ul id=book-search-results></ul></div><ul><li><a href=https://vericert.ymhg.org/coq-style-guide/>Coq Style Guide</a></li><li><a href=https://vericert.ymhg.org/docs/>Docs</a><ul><li><a href=https://vericert.ymhg.org/docs/building/>Building Vericert</a></li><li><a href=https://vericert.ymhg.org/docs/unreleased/ class=active>Unreleased Features</a></li><li><a href=https://vericert.ymhg.org/docs/using-vericert/>Using Vericert</a></li></ul></li><li><a href=https://vericert.ymhg.org/future/>Future Work</a></li></ul><ul><li><a href=https://github.com/ymherklotz/vericert target=_blank rel=noopener>Github</a></li></ul></nav><script>(function(){var menu=document.querySelector("aside.book-menu nav");addEventListener("beforeunload",function(event){localStorage.setItem("menu.scrollTop",menu.scrollTop);});menu.scrollTop=localStorage.getItem("menu.scrollTop");})();</script></aside><div class=book-page><header class=book-header><div class="flex align-center justify-between"><label for=menu-control><img src=/svg/menu.svg class=book-icon alt=Menu></label> <strong>Unreleased Features</strong> -<label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents><ul><li><ul><li><a href=#scheduling>Scheduling</a></li><li><a href=#scheduling>Operation Chaining</a></li><li><a href=#if-conversion>If-conversion</a></li><li><a href=#loop-pipelining>Loop pipelining</a></li><li><a href=#functions>Functions</a></li></ul></li></ul></nav></aside></header><h1>Unreleased Features</h1><article class=markdown><p>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:</p><ul><li><a href=#scheduling>scheduling</a>,</li><li><a href=#if-conversion>if-conversion</a>,</li><li><a href=#loop-pipelining>loop pipelining</a>, and</li><li><a href=#functions>functions</a>.</li></ul><p>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.</p><h2 id=scheduling>Scheduling +<label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents><ul><li><ul><li><a href=#scheduling>Scheduling</a></li><li><a href=#scheduling>Operation Chaining</a></li><li><a href=#if-conversion>If-conversion</a></li><li><a href=#loop-pipelining>Loop pipelining</a></li><li><a href=#functions>Functions</a></li></ul></li></ul></nav></aside></header><h1>Unreleased Features</h1><article class=markdown><p>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:</p><ul><li><a href=#scheduling>scheduling</a>,</li><li><a href=#if-conversion>if-conversion</a>,</li><li><a href=#loop-pipelining>loop pipelining</a>, and</li><li><a href=#functions>functions</a>.</li></ul><p>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.</p><h2 id=scheduling>Scheduling <a class=anchor href=#scheduling>#</a></h2><p>Scheduling is an optimisation which is used to run</p><h2 id=scheduling>Operation Chaining <a class=anchor href=#scheduling>#</a></h2><p>Scheduling is an optimisation which is used to run</p><h2 id=if-conversion>If-conversion <a class=anchor href=#if-conversion>#</a></h2><p>If-conversion</p><h2 id=loop-pipelining>Loop pipelining diff --git a/docs/using-vericert/index.html b/docs/using-vericert/index.html index 56a0c3a..9ededc8 100644 --- a/docs/using-vericert/index.html +++ b/docs/using-vericert/index.html @@ -3,7 +3,8 @@ void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) { in 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."><meta property="og:type" content="article"><meta property="og:url" content="https://vericert.ymhg.org/docs/using-vericert/"><title>Using Vericert |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.09c4470fdacb71a68922c07311d906b9cd808586067883b11db52f10e30e96d4.js integrity="sha256-CcRHD9rLcaaJIsBzEdkGuc2AhYYGeIOxHbUvEOMOltQ="></script></head><body><input type=checkbox class="hidden toggle" id=menu-control> <input type=checkbox class="hidden toggle" id=toc-control><main class="container flex"><aside class=book-menu><nav><div class=book-brand><a href=/><div id=book-logo></div><span></span></a><p>A formally verified high-level synthesis tool written in Coq.</p></div><div class=book-search><input type=text id=book-search-input placeholder=Search aria-label=Search maxlength=64 data-hotkeys=s/><div class="book-search-spinner hidden"></div><ul id=book-search-results></ul></div><ul><li><a href=https://vericert.ymhg.org/coq-style-guide/>Coq Style Guide</a></li><li><a href=https://vericert.ymhg.org/docs/>Docs</a><ul><li><a href=https://vericert.ymhg.org/docs/building/>Building Vericert</a></li><li><a href=https://vericert.ymhg.org/docs/unreleased/>Unreleased Features</a></li><li><a href=https://vericert.ymhg.org/docs/using-vericert/ class=active>Using Vericert</a></li></ul></li><li><a href=https://vericert.ymhg.org/future/>Future Work</a></li></ul><ul><li><a href=https://github.com/ymherklotz/vericert target=_blank rel=noopener>Github</a></li></ul></nav><script>(function(){var menu=document.querySelector("aside.book-menu nav");addEventListener("beforeunload",function(event){localStorage.setItem("menu.scrollTop",menu.scrollTop);});menu.scrollTop=localStorage.getItem("menu.scrollTop");})();</script></aside><div class=book-page><header class=book-header><div class="flex align-center justify-between"><label for=menu-control><img src=/svg/menu.svg class=book-icon alt=Menu></label> <strong>Using Vericert</strong> -<label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents></nav></aside></header><h1>Using Vericert</h1><article class=markdown><p>Vericert can be used to translate a subset of C into Verilog. As a simple example, consider the following C file (<code>main.c</code>):</p><div class=highlight><pre class=chroma><code class=language-C data-lang=C><span class=kt>void</span> <span class=nf>matrix_multiply</span><span class=p>(</span><span class=kt>int</span> <span class=n>first</span><span class=p>[</span><span class=mi>2</span><span class=p>][</span><span class=mi>2</span><span class=p>],</span> <span class=kt>int</span> <span class=n>second</span><span class=p>[</span><span class=mi>2</span><span class=p>][</span><span class=mi>2</span><span class=p>],</span> <span class=kt>int</span> <span class=n>multiply</span><span class=p>[</span><span class=mi>2</span><span class=p>][</span><span class=mi>2</span><span class=p>])</span> <span class=p>{</span> +<label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents></nav></aside></header><h1>Using Vericert</h1><article class=markdown><p>Vericert can be used to translate a subset of C into Verilog. As a simple example, consider the +following C file (<code>main.c</code>):</p><div class=highlight><pre class=chroma><code class=language-C data-lang=C><span class=kt>void</span> <span class=nf>matrix_multiply</span><span class=p>(</span><span class=kt>int</span> <span class=n>first</span><span class=p>[</span><span class=mi>2</span><span class=p>][</span><span class=mi>2</span><span class=p>],</span> <span class=kt>int</span> <span class=n>second</span><span class=p>[</span><span class=mi>2</span><span class=p>][</span><span class=mi>2</span><span class=p>],</span> <span class=kt>int</span> <span class=n>multiply</span><span class=p>[</span><span class=mi>2</span><span class=p>][</span><span class=mi>2</span><span class=p>])</span> <span class=p>{</span> <span class=kt>int</span> <span class=n>sum</span> <span class=o>=</span> <span class=mi>0</span><span class=p>;</span> <span class=k>for</span> <span class=p>(</span><span class=kt>int</span> <span class=n>c</span> <span class=o>=</span> <span class=mi>0</span><span class=p>;</span> <span class=n>c</span> <span class=o><</span> <span class=mi>2</span><span class=p>;</span> <span class=n>c</span><span class=o>++</span><span class=p>)</span> <span class=p>{</span> <span class=k>for</span> <span class=p>(</span><span class=kt>int</span> <span class=n>d</span> <span class=o>=</span> <span class=mi>0</span><span class=p>;</span> <span class=n>d</span> <span class=o><</span> <span class=mi>2</span><span class=p>;</span> <span class=n>d</span><span class=o>++</span><span class=p>)</span> <span class=p>{</span> @@ -24,12 +25,14 @@ void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) { in <span class=n>matrix_multiply</span><span class=p>(</span><span class=n>f</span><span class=p>,</span> <span class=n>s</span><span class=p>,</span> <span class=n>m</span><span class=p>);</span> <span class=k>return</span> <span class=n>m</span><span class=p>[</span><span class=mi>1</span><span class=p>][</span><span class=mi>1</span><span class=p>];</span> <span class=p>}</span> -</code></pre></div><p>It can be compiled using the following command, assuming that vericert is somewhere on the path.</p><pre><code class=language-nil data-lang=nil>vericert main.c -o main.v -</code></pre><p>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 <a href=http://iverilog.icarus.com/>Icarus Verilog</a> as an example:</p><pre><code class=language-nil data-lang=nil>iverilog -o main_v main.v -</code></pre><p>When executing, it should therefore print the following:</p><pre><code class=language-nil data-lang=nil>$ ./main_v -finished: 50 -</code></pre><p>This gives the same result as executing the C in the following way:</p><pre><code class=language-nil data-lang=nil>$ gcc -o main_c main.c +</code></pre></div><p>It can be compiled using the following command, assuming that vericert is somewhere on the path.</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>vericert main.c -o main.v +</code></pre></div><p>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 <a href=http://iverilog.icarus.com/>Icarus +Verilog</a> as an example:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>iverilog -o main_v main.v +</code></pre></div><p>When executing, it should therefore print the following:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>$ ./main_v +finished: <span class=m>50</span> +</code></pre></div><p>This gives the same result as executing the C in the following way:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>$ gcc -o main_c main.c $ ./main_c -$ echo $? -50 -</code></pre></article><footer class=book-footer><div class="flex flex-wrap justify-between"></div></footer><div class=book-comments></div><label for=menu-control class="hidden book-menu-overlay"></label></div><aside class=book-toc><nav id=TableOfContents></nav></aside></main></body></html>
\ No newline at end of file +$ <span class=nb>echo</span> <span class=nv>$?</span> +<span class=m>50</span> +</code></pre></div></article><footer class=book-footer><div class="flex flex-wrap justify-between"></div></footer><div class=book-comments></div><label for=menu-control class="hidden book-menu-overlay"></label></div><aside class=book-toc><nav id=TableOfContents></nav></aside></main></body></html>
\ No newline at end of file diff --git a/future/index.html b/future/index.html index e79cf0b..0b5fa7e 100644 --- a/future/index.html +++ b/future/index.html @@ -9,7 +9,8 @@ Type Support # type support Memory Partitioning # memory"><meta property="og:type" content="article"><meta property="og:url" content="https://vericert.ymhg.org/future/"><title>Future Work |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.09c4470fdacb71a68922c07311d906b9cd808586067883b11db52f10e30e96d4.js integrity="sha256-CcRHD9rLcaaJIsBzEdkGuc2AhYYGeIOxHbUvEOMOltQ="></script></head><body><input type=checkbox class="hidden toggle" id=menu-control> <input type=checkbox class="hidden toggle" id=toc-control><main class="container flex"><aside class=book-menu><nav><div class=book-brand><a href=/><div id=book-logo></div><span></span></a><p>A formally verified high-level synthesis tool written in Coq.</p></div><div class=book-search><input type=text id=book-search-input placeholder=Search aria-label=Search maxlength=64 data-hotkeys=s/><div class="book-search-spinner hidden"></div><ul id=book-search-results></ul></div><ul><li><a href=https://vericert.ymhg.org/coq-style-guide/>Coq Style Guide</a></li><li><a href=https://vericert.ymhg.org/docs/>Docs</a><ul><li><a href=https://vericert.ymhg.org/docs/building/>Building Vericert</a></li><li><a href=https://vericert.ymhg.org/docs/unreleased/>Unreleased Features</a></li><li><a href=https://vericert.ymhg.org/docs/using-vericert/>Using Vericert</a></li></ul></li><li><a href=https://vericert.ymhg.org/future/ class=active>Future Work</a></li></ul><ul><li><a href=https://github.com/ymherklotz/vericert target=_blank rel=noopener>Github</a></li></ul></nav><script>(function(){var menu=document.querySelector("aside.book-menu nav");addEventListener("beforeunload",function(event){localStorage.setItem("menu.scrollTop",menu.scrollTop);});menu.scrollTop=localStorage.getItem("menu.scrollTop");})();</script></aside><div class=book-page><header class=book-header><div class="flex align-center justify-between"><label for=menu-control><img src=/svg/menu.svg class=book-icon alt=Menu></label> <strong>Future Work</strong> -<label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents><ul><li><ul><li><a href=#globals>Globals</a></li><li><a href=#type-support>Type Support</a></li><li><a href=#memory-partitioning>Memory Partitioning</a></li></ul></li></ul></nav></aside></header><h1>Future Work</h1><article class=markdown><p>This section contains future work that should be added to Vericert to make it into a better high-level synthesis tool.</p><p>The next interesting optimisations that should be looked at are the following:</p><ul><li><a href=#globals>Globals</a></li><li><a href=#type-support>Type Support</a></li><li><a href=#memory-partitioning>Memory Partitioning</a></li><li><a href=/docs/unreleased/#scheduling>Operation Chaining</a></li></ul><h2 id=globals>Globals +<label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents><ul><li><ul><li><a href=#globals>Globals</a></li><li><a href=#type-support>Type Support</a></li><li><a href=#memory-partitioning>Memory Partitioning</a></li></ul></li></ul></nav></aside></header><h1>Future Work</h1><article class=markdown><p>This section contains future work that should be added to Vericert to make it into a better +high-level synthesis tool.</p><p>The next interesting optimisations that should be looked at are the following:</p><ul><li><a href=#globals>Globals</a></li><li><a href=#type-support>Type Support</a></li><li><a href=#memory-partitioning>Memory Partitioning</a></li><li><a href=/docs/unreleased/#scheduling>Operation Chaining</a></li></ul><h2 id=globals>Globals <a class=anchor href=#globals>#</a></h2><p>globals</p><h2 id=type-support>Type Support <a class=anchor href=#type-support>#</a></h2><p>type support</p><h2 id=memory-partitioning>Memory Partitioning <a class=anchor href=#memory-partitioning>#</a></h2><p>memory</p></article><footer class=book-footer><div class="flex flex-wrap justify-between"></div></footer><div class=book-comments></div><label for=menu-control class="hidden book-menu-overlay"></label></div><aside class=book-toc><nav id=TableOfContents><ul><li><ul><li><a href=#globals>Globals</a></li><li><a href=#type-support>Type Support</a></li><li><a href=#memory-partitioning>Memory Partitioning</a></li></ul></li></ul></nav></aside></main></body></html>
\ No newline at end of file @@ -2,8 +2,12 @@ Features # The project is currently a work in progress, so proofs remain to be finished. Currently, the following C features are supported, but are not all proven correct yet:"><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Vericert"><meta property="og:description" content><meta property="og:type" content="website"><meta property="og:url" content="https://vericert.ymhg.org/"><title>Vericert |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.09c4470fdacb71a68922c07311d906b9cd808586067883b11db52f10e30e96d4.js integrity="sha256-CcRHD9rLcaaJIsBzEdkGuc2AhYYGeIOxHbUvEOMOltQ="></script><link rel=alternate type=application/rss+xml href=https://vericert.ymhg.org/index.xml></head><body><input type=checkbox class="hidden toggle" id=menu-control> <input type=checkbox class="hidden toggle" id=toc-control><main class="container flex"><aside class=book-menu><nav><div class=book-brand><a href=/><div id=book-logo></div><span></span></a><p>A formally verified high-level synthesis tool written in Coq.</p></div><div class=book-search><input type=text id=book-search-input placeholder=Search aria-label=Search maxlength=64 data-hotkeys=s/><div class="book-search-spinner hidden"></div><ul id=book-search-results></ul></div><ul><li><a href=https://vericert.ymhg.org/coq-style-guide/>Coq Style Guide</a></li><li><a href=https://vericert.ymhg.org/docs/>Docs</a><ul><li><a href=https://vericert.ymhg.org/docs/building/>Building Vericert</a></li><li><a href=https://vericert.ymhg.org/docs/unreleased/>Unreleased Features</a></li><li><a href=https://vericert.ymhg.org/docs/using-vericert/>Using Vericert</a></li></ul></li><li><a href=https://vericert.ymhg.org/future/>Future Work</a></li></ul><ul><li><a href=https://github.com/ymherklotz/vericert target=_blank rel=noopener>Github</a></li></ul></nav><script>(function(){var menu=document.querySelector("aside.book-menu nav");addEventListener("beforeunload",function(event){localStorage.setItem("menu.scrollTop",menu.scrollTop);});menu.scrollTop=localStorage.getItem("menu.scrollTop");})();</script></aside><div class=book-page><header class=book-header><div class="flex align-center justify-between"><label for=menu-control><img src=/svg/menu.svg class=book-icon alt=Menu></label> <strong>Vericert</strong> -<label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents><ul><li><ul><li><a href=#features>Features</a></li><li><a href=#content>Content</a></li><li><a href=#papers>Papers</a></li></ul></li></ul></nav></aside></header><h1>Vericert</h1><article class=markdown><p>A formally verified high-level synthesis (HLS) tool written in Coq, building on top of <a href=https://github.com/AbsInt/CompCert>CompCert</a>. This ensures the correctness of the C to Verilog translation according to our Verilog semantics and CompCert’s C semantics, removing the need to check the resulting hardware for behavioural correctness.</p><h2 id=features>Features -<a class=anchor href=#features>#</a></h2><p>The project is currently a work in progress, so proofs remain to be finished. Currently, the following C features are supported, but are not all proven correct yet:</p><ul><li>all int operations,</li><li>non-recursive function calls,</li><li>local arrays and pointers</li><li>control-flow structures such as if-statements, for-loops, etc…</li></ul><h2 id=content>Content +<label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents><ul><li><ul><li><a href=#features>Features</a></li><li><a href=#content>Content</a></li><li><a href=#papers>Papers</a></li></ul></li></ul></nav></aside></header><h1>Vericert</h1><article class=markdown><p>A formally verified high-level synthesis (HLS) tool written in Coq, building on top of <a href=https://github.com/AbsInt/CompCert>CompCert</a>. +This ensures the correctness of the C to Verilog translation according to our Verilog semantics and +CompCert’s C semantics, removing the need to check the resulting hardware for behavioural +correctness.</p><h2 id=features>Features +<a class=anchor href=#features>#</a></h2><p>The project is currently a work in progress, so proofs remain to be finished. Currently, the +following C features are supported, but are not all proven correct yet:</p><ul><li>all int operations,</li><li>non-recursive function calls,</li><li>local arrays and pointers</li><li>control-flow structures such as if-statements, for-loops, etc…</li></ul><h2 id=content>Content <a class=anchor href=#content>#</a></h2><ul><li><a href=/docs/building/>Vericert Documentation</a></li></ul><h2 id=papers>Papers <a class=anchor href=#papers>#</a></h2><dl><dt>OOPSLA ‘21</dt><dd>Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. Formal Verification of High-Level Synthesis. In <em>Proc. ACM Program. Lang.</em> 5, OOPSLA, 2021. [<a href=/papers/fvhls_oopsla21.pdf>pdf</a>]</dd><dt>LATTE ‘21</dt><dd>Yann Herklotz and John Wickerson. High-level synthesis tools should be proven |