Start converting comments

3 files changed, 45 insertions, 85 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index b907629..7aef71c 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -1,7 +1,3 @@
-(*|
-.. coq:: none
-|*)
-
 (*
  * Vericert: Verified high-level synthesis.
  * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
@@ -20,21 +16,15 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(*|
-==============
-Compiler Proof
-==============
-
-.. contents:: Table of Contents
-   :depth: 2
+(** * Compiler Proof
 
-This is the top-level module of the correctness proof and proves the final backwards simulation correct.
+This is the top-level module of the correctness proof and proves the final backwards simulation
+correct.
 
-Imports
-=======
+** Imports
 
-We first need to import all of the modules that are used in the correctness proof, which includes all of the passes that are performed in Vericert and the CompCert front end.
-|*)
+We first need to import all of the modules that are used in the correctness proof, which includes
+all of the passes that are performed in Vericert and the CompCert front end.  *)
 
 Require compcert.backend.Selection.
 Require compcert.backend.RTL.
@@ -75,12 +65,10 @@ Require vericert.hls.Memorygen.
 
 Require Import vericert.hls.HTLgenproof.
 
-(*|
-Declarations
-============
+(** ** Declarations
 
-We then need to declare the external OCaml functions used to print out intermediate steps in the compilation, such as ``print_RTL``, ``print_HTL`` and ``print_RTLBlock``.
-|*)
+We then need to declare the external OCaml functions used to print out intermediate steps in the
+compilation, such as ``print_RTL``, ``print_HTL`` and ``print_RTLBlock``.  *)
 
 Parameter print_RTL: Z -> RTL.program -> unit.
 Parameter print_HTL: Z -> HTL.program -> unit.
@@ -98,18 +86,16 @@ Proof.
   intros; unfold print. destruct (printer prog); auto.
 Qed.
 
-(*|
-We also declare some new notation, which is also used in CompCert to combine the monadic results of each pass.
-|*)
+(** We also declare some new notation, which is also used in CompCert to combine the monadic results
+of each pass.  *)
 
 Notation "a @@@ b" :=
    (Compiler.apply_partial _ _ a b) (at level 50, left associativity).
 Notation "a @@ b" :=
   (Compiler.apply_total _ _ a b) (at level 50, left associativity).
 
-(*|
-As printing is used in the translation but does not change the output, we need to prove that it has no effect so that it can be removed during the proof.
-|*)
+(** As printing is used in the translation but does not change the output, we need to prove that it
+has no effect so that it can be removed during the proof.  *)
 
 Lemma compose_print_identity:
   forall (A: Type) (x: res A) (f: A -> unit),
@@ -118,9 +104,8 @@ Proof.
   intros. destruct x; simpl. rewrite print_identity. auto. auto.
 Qed.
 
-(*|
-Finally, some optimisation passes are only activated by a flag, which is handled by the following functions for partial and total passes.
-|*)
+(** Finally, some optimisation passes are only activated by a flag, which is handled by the following
+functions for partial and total passes.  *)
 
 Definition total_if {A: Type}
           (flag: unit -> bool) (f: A -> A) (prog: A) : A :=
@@ -171,12 +156,11 @@ Proof.
   intros. unfold match_if in *. destruct (flag tt). eauto. subst. apply forward_simulation_identity.
 Qed.
 
-(*|
-Top-level Translation
----------------------
+(** *** Top-level Translation
 
-An optimised transformation function from ``RTL`` to ``Verilog`` can then be defined, which applies the front end compiler optimisations of CompCert to the RTL that is generated and then performs the two Vericert passes from RTL to HTL and then from HTL to Verilog.
-|*)
+An optimised transformation function from ``RTL`` to ``Verilog`` can then be defined, which applies
+the front end compiler optimisations of CompCert to the RTL that is generated and then performs the
+two Vericert passes from RTL to HTL and then from HTL to Verilog.  *)
 
 Definition transf_backend (r : RTL.program) : res Verilog.program :=
   OK r
@@ -200,9 +184,8 @@ Definition transf_backend (r : RTL.program) : res Verilog.program :=
    @@ print (print_HTL 1)*)
    @@ Veriloggen.transl_program.
 
-(*|
-The transformation functions from RTL to Verilog are then added to the backend of the CompCert transformations from Clight to RTL.
-|*)
+(** The transformation functions from RTL to Verilog are then added to the backend of the CompCert
+transformations from Clight to RTL.  *)
 
 Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
   OK p
@@ -215,10 +198,6 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_RTL 0)
   @@@ transf_backend.
 
-(*|
-.. coq:: none
-|*)
-
 (* This is an unverified version of transf_hls with some experimental additions such as scheduling
 that aren't completed yet. *)
 Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
@@ -255,12 +234,10 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_HTL 0)
    @@ Veriloggen.transl_program.
 
-(*|
-Correctness Proof
-=================
+(** ** Correctness Proof
 
-Finally, the top-level definition for all the passes is defined, which combines the ``match_prog`` predicates of each translation pass from C until Verilog.
-|*)
+Finally, the top-level definition for all the passes is defined, which combines the ``match_prog``
+predicates of each translation pass from C until Verilog.  *)
 
 Local Open Scope linking_scope.
 
@@ -283,16 +260,14 @@ Definition CompCert's_passes :=
   ::: mkpass Veriloggenproof.match_prog
   ::: pass_nil _.
 
-(*|
-These passes are then composed into a larger, top-level ``match_prog`` predicate which matches a C program directly with a Verilog program.
-|*)
+(** These passes are then composed into a larger, top-level ``match_prog`` predicate which matches a
+C program directly with a Verilog program.  *)
 
 Definition match_prog: Csyntax.program -> Verilog.program -> Prop :=
   pass_match (compose_passes CompCert's_passes).
 
-(*|
-We then need to prove that this predicate holds, assuming that the translation is performed using the ``transf_hls`` function declared above.
-|*)
+(** We then need to prove that this predicate holds, assuming that the translation is performed
+using the ``transf_hls`` function declared above.  *)
 
 Theorem transf_hls_match:
   forall p tp,
@@ -394,12 +369,12 @@ Ltac DestructM :=
   apply Verilog.semantics_determinate.
 Qed.
 
-(*|
-Backward Simulation
--------------------
+(** *** Backward Simulation
 
-The following theorem is a *backward simulation* between the C and Verilog, which proves the semantics preservation of the translation.  We can assume that the C and Verilog programs match, as we have proven previously in ``transf_hls_match`` that our translation implies that the ``match_prog`` predicate will hold.
-|*)
+The following theorem is a *backward simulation* between the C and Verilog, which proves the
+semantics preservation of the translation.  We can assume that the C and Verilog programs match, as
+we have proven previously in ``transf_hls_match`` that our translation implies that the
+``match_prog`` predicate will hold.  *)
 
 Theorem c_semantic_preservation:
   forall p tp,
@@ -416,9 +391,8 @@ Proof.
   exact (proj2 (cstrategy_semantic_preservation _ _ H)).
 Qed.
 
-(*|
-We can then use ``transf_hls_match`` to prove the backward simulation where the assumption is that the translation is performed using the ``transf_hls`` function and that it succeeds.
-|*)
+(** We can then use ``transf_hls_match`` to prove the backward simulation where the assumption is
+that the translation is performed using the ``transf_hls`` function and that it succeeds.  *)
 
 Theorem transf_c_program_correct:
   forall p tp,
@@ -428,9 +402,9 @@ Proof.
   intros. apply c_semantic_preservation. apply transf_hls_match; auto.
 Qed.
 
-(*|
-The final theorem of the semantic preservation of the translation of separate translation units can also be proven correct, however, this is only because the translation fails if more than one translation unit is passed to Vericert at the moment.
-|*)
+(** The final theorem of the semantic preservation of the translation of separate translation units
+can also be proven correct, however, this is only because the translation fails if more than one
+translation unit is passed to Vericert at the moment.  *)
 
 Theorem separate_transf_c_program_correct:
   forall c_units verilog_units c_program,
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 4585770..9b8f4d4 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -30,14 +30,10 @@ Require Import vericert.bourdoncle.Bourdoncle.
 
 Parameter build_bourdoncle : function -> (bourdoncle * PMap.t N).
 
-(*|
-=============
-If conversion
-=============
+(** * If conversion
 
 This conversion is a verified conversion from RTLBlock back to itself, which performs if-conversion
-on basic blocks to make basic blocks larger.
-|*)
+on basic blocks to make basic blocks larger.  *)
 
 Definition combine_pred (p: pred_op) (optp: option pred_op) :=
   match optp with
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 58b048c..82f3f5e 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -34,24 +34,17 @@ Require Import vericert.hls.Predicate.
 Require Import vericert.hls.Abstr.
 Import NE.NonEmptyNotation.
 
-(*|
-=================
-RTLPar Generation
-=================
-|*)
+(** * RTLPar Generation *)
 
 #[local] Open Scope positive.
 #[local] Open Scope forest.
 #[local] Open Scope pred_op.
 
-(*|
-Abstract Computations
-=====================
+(** ** Abstract Computations
 
 Define the abstract computation using the ``update`` function, which will set each register to its
 symbolic value.  First we need to define a few helper functions to correctly translate the
-predicates.
-|*)
+predicates.  *)
 
 Fixpoint list_translation (l : list reg) (f : forest) {struct l} : list pred_expr :=
   match l with
@@ -146,9 +139,7 @@ Definition app_predicated {A: Type} (p: option pred_op) (a b: predicated A) :=
 Definition pred_ret {A: Type} (a: A) : predicated A :=
   NE.singleton (T, a).
 
-(*|
-Update Function
----------------
+(** *** Update Function
 
 The ``update`` function will generate a new forest given an existing forest and a new instruction,
 so that it can evaluate a symbolic expression by folding over a list of instructions.  The main
@@ -158,8 +149,7 @@ problem is that predicates need to be merged as well, so that:
 2. The expression assigned to the register should still be correct.
 
 This is done by multiplying the predicates together, and assigning the negation of the expression to
-the other predicates.
-|*)
+the other predicates.  *)
 
 Definition update (f : forest) (i : instr) : forest :=
   match i with