Fix up some more documentation

7 files changed, 68 insertions, 146 deletions

diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index 2ab79cf..01f2fd9 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -38,14 +38,11 @@ Require Import vericert.hls.Predicate.
 #[local] Open Scope positive.
 #[local] Open Scope pred_op.
 
-(*|
-Schedule Oracle
-===============
+(** ** Schedule Oracle
 
 This oracle determines if a schedule was valid by performing symbolic execution on the input and
 output and showing that these behave the same.  This acts on each basic block separately, as the
-rest of the functions should be equivalent.
-|*)
+rest of the functions should be equivalent.  *)
 
 Definition reg := positive.
 
@@ -54,10 +51,8 @@ Inductive resource : Set :=
 | Pred : reg -> resource
 | Mem : resource.
 
-(*|
-The following defines quite a few equality comparisons automatically, however, these can be
-optimised heavily if written manually, as their proofs are not needed.
-|*)
+(** The following defines quite a few equality comparisons automatically, however, these can be
+optimised heavily if written manually, as their proofs are not needed.  *)
 
 Lemma resource_eq : forall (r1 r2 : resource), {r1 = r2} + {r1 <> r2}.
 Proof.
@@ -179,11 +174,9 @@ Proof.
   repeat decide equality.
 Defined.
 
-(*|
-We then create equality lemmas for a resource and a module to index resources uniquely.  The
+(** We then create equality lemmas for a resource and a module to index resources uniquely.  The
 indexing is done by setting Mem to 1, whereas all other infinitely many registers will all be
-shifted right by 1.  This means that they will never overlap.
-|*)
+shifted right by 1.  This means that they will never overlap.  *)
 
 Module R_indexed.
   Definition t := resource.
@@ -200,8 +193,7 @@ Module R_indexed.
   Definition eq := resource_eq.
 End R_indexed.
 
-(*|
-We can then create expressions that mimic the expressions defined in RTLBlock and RTLPar, which use
+(** We can then create expressions that mimic the expressions defined in RTLBlock and RTLPar, which use
 expressions instead of registers as their inputs and outputs.  This means that we can accumulate all
 the results of the operations as general expressions that will be present in those registers.
 
@@ -211,8 +203,7 @@ the results of the operations as general expressions that will be present in tho
 - Estore: A store from a register to a memory location.
 
 Then, to make recursion over expressions easier, expression_list is also defined in the datatype, as
-that enables mutual recursive definitions over the datatypes.
-|*)
+that enables mutual recursive definitions over the datatypes.  *)
 
 Inductive expression : Type :=
 | Ebase : resource -> expression
@@ -321,10 +312,8 @@ Definition predicated A := NE.non_empty (pred_op * A).
 
 Definition pred_expr := predicated expression.
 
-(*|
-Using IMap we can create a map from resources to any other type, as resources can be uniquely
-identified as positive numbers.
-|*)
+(** Using IMap we can create a map from resources to any other type, as resources can be uniquely
+identified as positive numbers.  *)
 
 Module Rtree := ITree(R_indexed).
 
@@ -356,10 +345,8 @@ Definition get_m i := match i with mk_instr_state a b c => c end.
 Definition eval_predf_opt pr p :=
   match p with Some p' => eval_predf pr p' | None => true end.
 
-(*|
-Finally we want to define the semantics of execution for the expressions with symbolic values, so
-the result of executing the expressions will be an expressions.
-|*)
+(** Finally we want to define the semantics of execution for the expressions with symbolic values,
+so the result of executing the expressions will be an expressions.  *)
 
 Section SEMANTICS.
 
@@ -682,7 +669,7 @@ Inductive similar {A B} : @ctx A -> @ctx B -> Prop :=
 
 Definition beq_pred_expr_once (pe1 pe2: pred_expr) : bool :=
   match pe1, pe2 with
-  (*| PEsingleton None e1, PEsingleton None e2 => beq_expression e1 e2
+  (* PEsingleton None e1, PEsingleton None e2 => beq_expression e1 e2
   | PEsingleton (Some p1) e1, PEsingleton (Some p2) e2 =>
     if beq_expression e1 e2
     then match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with
diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 551c66e..47f2092 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -36,13 +36,10 @@ Require Import ValueInt.
 
 Local Open Scope positive.
 
-(*|
-The purpose of the hardware transfer language (HTL) is to create a more
-hardware-like layout that is still similar to the register transfer language
-(RTL) that it came from. The main change is that function calls become module
-instantiations and that we now describe a state machine instead of a
-control-flow graph.
-|*)
+(** The purpose of the hardware transfer language (HTL) is to create a more hardware-like layout
+that is still similar to the register transfer language (RTL) that it came from. The main change is
+that function calls become module instantiations and that we now describe a state machine instead of
+a control-flow graph.  *)
 
 Local Open Scope assocmap.
 
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index c7dbe72..265b8f7 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -160,7 +160,7 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
       translate_arr_access mem addr args stk s = OK c s' i ->
       tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src))
                (state_goto st n).
-(*| tr_instr_Ijumptable :
+(* tr_instr_Ijumptable :
     forall cexpr tbl r,
     cexpr = tbl_to_case_expr st tbl ->
     tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).*)
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index d9f3e74..7eabcf7 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -31,22 +31,18 @@ Require Import compcert.verilog.Op.
 Require Import Predicate.
 Require Import Vericertlib.
 
-(*|
-=====================
-RTLBlock Instructions
-=====================
+(** * RTLBlock Instructions
 
 These instructions are used for ``RTLBlock`` and ``RTLPar``, so that they have consistent
 instructions, which greatly simplifies the proofs, as they will by default have the same instruction
 syntax and semantics.  The only changes are therefore at the top-level of the instructions.
 
-Instruction Definition
-======================
+** Instruction Definition
 
 First, we define the instructions that can be placed into a basic block, meaning they won't branch.
 The main changes to how instructions are defined in ``RTL``, is that these instructions don't have a
 next node, as they will be in a basic block, and they also have an optional predicate (``pred_op``).
-|*)
+*)
 
 Definition node := positive.
 
@@ -57,13 +53,10 @@ Inductive instr : Type :=
 | RBstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
 | RBsetpred : option pred_op -> condition -> list reg -> predicate -> instr.
 
-(*|
-Control-Flow Instruction Definition
-===================================
+(** ** Control-Flow Instruction Definition
 
 These are the instructions that count as control-flow, and will be placed at the end of the basic
-blocks.
-|*)
+blocks.  *)
 
 Inductive cf_instr : Type :=
 | RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr
@@ -76,10 +69,7 @@ Inductive cf_instr : Type :=
 | RBgoto : node -> cf_instr
 | RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr.
 
-(*|
-Helper functions
-================
-|*)
+(** ** Helper functions  *)
 
 Fixpoint successors_instr (i : cf_instr) : list node :=
   match i with
@@ -170,17 +160,14 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
   | _, _ => Regmap.init Vundef
   end.
 
-(*|
-Instruction State
------------------
+(** *** Instruction State
 
 Definition of the instruction state, which contains the following:
 
-:is_rs: This is the current state of the registers.
-:is_ps: This is the current state of the predicate registers, which is in a separate namespace and
-        area compared to the standard registers in ``is_rs``.
-:is_mem: The current state of the memory.
-|*)
+- [is_rs] This is the current state of the registers.
+- [is_ps] This is the current state of the predicate registers, which is in a separate namespace and
+        area compared to the standard registers in [is_rs].
+- [is_mem] The current state of the memory.  *)
 
 Record instr_state := mk_instr_state {
   is_rs: regset;
@@ -188,10 +175,7 @@ Record instr_state := mk_instr_state {
   is_mem: mem;
 }.
 
-(*|
-Top-Level Type Definitions
-==========================
-|*)
+(** ** Top-Level Type Definitions *)
 
 Section DEFINITION.
 
@@ -256,10 +240,7 @@ Section DEFINITION.
 
 End DEFINITION.
 
-(*|
-Semantics
-=========
-|*)
+(** ** Semantics *)
 
 Section RELSEM.
 
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 82f3f5e..ab4c0da 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -42,7 +42,7 @@ Import NE.NonEmptyNotation.
 
 (** ** Abstract Computations
 
-Define the abstract computation using the ``update`` function, which will set each register to its
+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.  *)
 
@@ -141,7 +141,7 @@ Definition pred_ret {A: Type} (a: A) : predicated A :=
 
 (** *** Update Function
 
-The ``update`` function will generate a new forest given an existing forest and a new instruction,
+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
 problem is that predicates need to be merged as well, so that:
 
@@ -181,12 +181,10 @@ Definition update (f : forest) (i : instr) : forest :=
        (map_predicated (pred_ret (Esetpred c)) (merge (list_translation args f))))
   end.
 
-(*|
-Implementing which are necessary to show the correctness of the translation validation by showing
-that there aren't any more effects in the resultant RTLPar code than in the RTLBlock code.
+(** Implementing which are necessary to show the correctness of the translation validation by
+showing that there aren't any more effects in the resultant RTLPar code than in the RTLBlock code.
 
-Get a sequence from the basic block.
-|*)
+Get a sequence from the basic block.  *)
 
 Fixpoint abstract_sequence (f : forest) (b : list instr) : forest :=
   match b with
@@ -194,18 +192,15 @@ Fixpoint abstract_sequence (f : forest) (b : list instr) : forest :=
   | i :: l => abstract_sequence (update f i) l
   end.
 
-(*|
-Check equivalence of control flow instructions.  As none of the basic blocks should have been moved,
-none of the labels should be different, meaning the control-flow instructions should match exactly.
-|*)
+(** Check equivalence of control flow instructions.  As none of the basic blocks should have been
+moved, none of the labels should be different, meaning the control-flow instructions should match
+exactly.  *)
 
 Definition check_control_flow_instr (c1 c2: cf_instr) : bool :=
   if cf_instr_eq c1 c2 then true else false.
 
-(*|
-We define the top-level oracle that will check if two basic blocks are equivalent after a scheduling
-transformation.
-|*)
+(** We define the top-level oracle that will check if two basic blocks are equivalent after a
+scheduling transformation.  *)
 
 Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool :=
   match bb with
@@ -246,10 +241,7 @@ Lemma check_scheduled_trees_correct2:
     PTree.get x f2 = None.
 Proof. solve_scheduled_trees_correct. Qed.
 
-(*|
-Top-level Functions
-===================
-|*)
+(** ** Top-level Functions  *)
 
 Parameter schedule : RTLBlock.function -> RTLPar.function.
 
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index 588f67f..0023edc 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -46,12 +46,9 @@ Inductive state_lessdef : instr_state -> instr_state -> Prop :=
     (forall x, rs1 !! x = rs2 !! x) ->
     state_lessdef (mk_instr_state rs1 m1) (mk_instr_state rs2 m1).
 
-(*|
-RTLBlock to abstract translation
---------------------------------
+(** *** RTLBlock to abstract translation
 
-Correctness of translation from RTLBlock to the abstract interpretation language.
-|*)
+Correctness of translation from RTLBlock to the abstract interpretation language. *)
 
 Ltac inv_simp :=
   repeat match goal with
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index 3a2c81d..7561f77 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -142,30 +142,23 @@ Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
 Inductive scl_decl : Type := VScalar (sz : nat).
 Inductive arr_decl : Type := VArray (sz : nat) (ln : nat).
 
-(*|
-Verilog AST
-===========
+(** ** Verilog AST
 
 The Verilog AST is defined here, which is the target language of the
 compilation.
 
-Value
------
+*** Value
 
 The Verilog [value] is a bitvector containg a size and the actual bitvector. In
 this case, the [Word.word] type is used as many theorems about that bitvector
 have already been proven.
-|*)
 
-(*|
-Binary Operators
-----------------
+*** Binary Operators
 
 These are the binary operations that can be represented in Verilog. Ideally,
 multiplication and division would be done by custom modules which could al so be
 scheduled properly. However, for now every Verilog operator is assumed to take
-one clock cycle.
-|*)
+one clock cycle.  *)
 
 Inductive binop : Type :=
 | Vadd : binop  (** addition (binary [+]) *)
@@ -191,21 +184,15 @@ Inductive binop : Type :=
 | Vshl : binop  (** shift left ([<<]) *)
 | Vshr : binop (** shift right ([>>>]) *)
 | Vshru : binop. (** shift right unsigned ([>>]) *)
-(*| Vror : binop (** shift right unsigned ([>>]) *)*)
+(* Vror : binop (** shift right unsigned ([>>]) *)*)
 
-(*|
-Unary Operators
----------------
-|*)
+(** *** Unary Operators *)
 
 Inductive unop : Type :=
 | Vneg  (** negation ([-]) *)
 | Vnot. (** not operation [!] *)
 
-(*|
-Expressions
------------
-|*)
+(** *** Expressions *)
 
 Inductive expr : Type :=
 | Vlit : value -> expr
@@ -220,10 +207,7 @@ Inductive expr : Type :=
 Definition posToExpr (p : positive) : expr :=
   Vlit (posToValue p).
 
-(*|
-Statements
-----------
-|*)
+(** *** Statements *)
 
 Inductive stmnt : Type :=
 | Vskip : stmnt
@@ -236,17 +220,13 @@ with stmnt_expr_list : Type :=
 | Stmntnil : stmnt_expr_list
 | Stmntcons : expr -> stmnt -> stmnt_expr_list -> stmnt_expr_list.
 
-(*|
-Edges
------
+(** *** Edges
 
-These define when an always block should be triggered, for example if the always
-block should be triggered synchronously at the clock edge, or asynchronously for
-combinational logic.
+These define when an always block should be triggered, for example if the always block should be
+triggered synchronously at the clock edge, or asynchronously for combinational logic.
 
-[edge] is not part of [stmnt] in this formalisation because is closer to the
-semantics that are used.
-|*)
+[edge] is not part of [stmnt] in this formalisation because is closer to the semantics that are
+used.  *)
 
 Inductive edge : Type :=
 | Vposedge : reg -> edge
@@ -254,14 +234,11 @@ Inductive edge : Type :=
 | Valledge : edge
 | Voredge : edge -> edge -> edge.
 
-(*|
-Module Items
-------------
+(** *** Module Items
 
-Module items can either be declarations ([Vdecl]) or always blocks ([Valways]).
-The declarations are always register declarations as combinational logic can be
-done using combinational always block instead of continuous assignments.
-|*)
+Module items can either be declarations ([Vdecl]) or always blocks ([Valways]).  The declarations
+are always register declarations as combinational logic can be done using combinational always block
+instead of continuous assignments.  *)
 
 Inductive io : Type :=
 | Vinput : io
@@ -278,8 +255,7 @@ Inductive module_item : Type :=
 | Valways_ff : edge -> stmnt -> module_item
 | Valways_comb : edge -> stmnt -> module_item.
 
-(*|
-The main module type containing all the important control signals
+(** The main module type containing all the important control signals
 
 - [mod_start] If set, starts the computations in the module.
 - [mod_reset] If set, reset the state in the module.
@@ -287,8 +263,7 @@ The main module type containing all the important control signals
 - [mod_args] The arguments to the module.
 - [mod_finish] Bit that is set if the result is ready.
 - [mod_return] The return value that was computed.
-- [mod_body] The body of the module, including the state machine.
-|*)
+- [mod_body] The body of the module, including the state machine.  *)
 
 Record module : Type := mkmodule {
   mod_start : reg;
@@ -308,21 +283,17 @@ Definition fundef := AST.fundef module.
 
 Definition program := AST.program fundef unit.
 
-(*|
-Convert a [positive] to an expression directly, setting it to the right size.
-|*)
+(** Convert a [positive] to an expression directly, setting it to the right size.  *)
 Definition posToLit (p : positive) : expr :=
   Vlit (posToValue p).
 
 Definition fext := unit.
 Definition fextclk := nat -> fext.
 
-(*|
-State
------
+(** *** State
 
 The [state] contains the following items:
-n
+
 - Current [module] that is being worked on, so that the state variable can be
 retrieved and set appropriately.
 - Current [module_item] which is being worked on.
@@ -338,8 +309,7 @@ retrieved and set appropriately.
   Verilog, as the Verilog was generated by the RTL, which means that we have to
   make an assumption about how it looks.  In this case, that it contains state
   which determines which part of the Verilog is executed.  This is then the part
-  of the Verilog that should match with the RTL.
-|*)
+  of the Verilog that should match with the RTL.  *)
 
 Inductive stackframe : Type :=
   Stackframe :
@@ -459,9 +429,7 @@ Definition handle_def {A : Type} (a : A) (val : option A)
 
 Local Open Scope error_monad_scope.
 
-(*|
-Return the location of the lhs of an assignment.
-|*)
+(** Return the location of the lhs of an assignment.  *)
 
 Inductive location : Type :=
 | LocReg (_ : reg)