Remove literal files again

21 files changed, 570 insertions, 273 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index 8882686..cd05aa9 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -16,15 +16,21 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(** * Compiler Proof
+(*|
+==============
+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.
@@ -65,10 +71,14 @@ 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.
@@ -86,16 +96,20 @@ 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),
@@ -104,8 +118,10 @@ 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 :=
@@ -156,11 +172,15 @@ 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
@@ -184,8 +204,10 @@ 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
@@ -234,10 +256,13 @@ 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.
 
@@ -260,14 +285,18 @@ 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,
@@ -369,12 +398,16 @@ 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,
@@ -391,8 +424,11 @@ 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,
@@ -402,9 +438,12 @@ 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/bourdoncle/Bourdoncle.v b/src/bourdoncle/Bourdoncle.v
index 9d470b7..ef1798a 100644
--- a/src/bourdoncle/Bourdoncle.v
+++ b/src/bourdoncle/Bourdoncle.v
@@ -1,4 +1,6 @@
-(** Type of a Bourdoncle component. *)
+(*|
+Type of a Bourdoncle component.
+|*)
 
 Require Import List.
 Require Import BinPos.
diff --git a/src/common/Maps.v b/src/common/Maps.v
index 13ca276..cb9dc2c 100644
--- a/src/common/Maps.v
+++ b/src/common/Maps.v
@@ -29,8 +29,9 @@ Import PTree.
 
 Local Open Scope error_monad_scope.
 
-(** Instance of traverse for [PTree] and [Errors]. This should maybe be generalised
-    in the future. *)
+(*|
+Instance of traverse for ``PTree`` and ``Errors``. This should maybe be generalised in the future.
+|*)
 
 Module PTree.
 
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index 43d7783..9d310fb 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -38,11 +38,14 @@ 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.  *)
+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.
+|*)
 
 Definition reg := positive.
 
@@ -51,8 +54,11 @@ 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.
@@ -174,9 +180,12 @@ Proof.
   repeat decide equality.
 Defined.
 
-(** 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.  *)
+(*|
+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.
+|*)
 
 Module R_indexed.
   Definition t := resource.
@@ -193,17 +202,21 @@ 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
-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.
+(*|
+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.
 
 - Ebase: the starting value of the register.
 - Eop: Some arithmetic operation on a number of registers.
 - Eload: A load from a memory location into a register.
 - 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.  *)
+Then, to make recursion over expressions easier, expression_list is also defined
+in the datatype, as that enables mutual recursive definitions over the
+datatypes.
+|*)
 
 Inductive expression : Type :=
 | Ebase : resource -> expression
@@ -312,8 +325,10 @@ 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).
 
@@ -345,8 +360,11 @@ 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.
 
diff --git a/src/hls/Array.v b/src/hls/Array.v
index 0f5ae02..de74611 100644
--- a/src/hls/Array.v
+++ b/src/hls/Array.v
@@ -190,7 +190,10 @@ Proof.
   auto using nth_error_nth.
 Qed.
 
-(** Tail recursive version of standard library function. *)
+(*|
+Tail recursive version of standard library function.
+|*)
+
 Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A :=
   match n with
   | O => acc
diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 47f2092..f3af3d8 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -36,10 +36,13 @@ 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.
 
@@ -84,7 +87,10 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
 Definition empty_stack (m : module) : Verilog.assocmap_arr :=
   (AssocMap.set m.(mod_ram).(ram_mem) (Array.arr_repeat None m.(mod_ram).(ram_size)) (AssocMap.empty Verilog.arr)).
 
-(** * Operational Semantics *)
+(*|
+Operational Semantics
+=====================
+|*)
 
 Definition genv := Globalenvs.Genv.t fundef unit.
 
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 8c85701..8960ef9 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -405,7 +405,10 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg)
   | _, _ => error (Errors.msg "HTLPargen: translate_eff_addressing unsuported addressing")
   end.
 
-(** Translate an instruction to a statement. FIX mulhs mulhu *)
+(*|
+Translate an instruction to a statement. FIX mulhs mulhu
+|*)
+
 Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
   match op, args with
   | Op.Omove, r::nil => ret (Vvar r)
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index bf4b057..bf1ef1c 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -1004,22 +1004,25 @@ Section CORRECTNESS.
         constructor.
   Qed.
 
-  (** The proof of semantic preservation for the translation of instructions
-      is a simulation argument based on diagrams of the following form:
-<<
-                      match_states
-    code st rs ------------------------- State m st assoc
-         ||                                      |
-         ||                                      |
-         ||                                      |
-         \/                                      v
-    code st rs' ------------------------ State m st assoc'
-                      match_states
->>
-      where [tr_code c data control fin rtrn st] is assumed to hold.
-
-      The precondition and postcondition is that that should hold is [match_assocmaps rs assoc].
-   *)
+(*|
+The proof of semantic preservation for the translation of instructions is a
+simulation argument based on diagrams of the following form:
+
+::
+>                      match_states
+>    code st rs ------------------------- State m st assoc
+>         ||                                      |
+>         ||                                      |
+>         ||                                      |
+>         \/                                      v
+>    code st rs' ------------------------ State m st assoc'
+>                      match_states
+
+where ``tr_code c data control fin rtrn st`` is assumed to hold.
+
+The precondition and postcondition is that that should hold is ``match_assocmaps
+rs assoc``.
+|*)
 
   Definition transl_instr_prop (instr : RTL.instruction) : Prop :=
     forall m asr asa fin rtrn st stmt trans res,
@@ -1091,7 +1094,7 @@ Section CORRECTNESS.
     apply Smallstep.plus_one.
     eapply HTL.step_module; eauto.
     inv CONST; assumption.
-    inv CONST; assumption. 
+    inv CONST; assumption.
     (* processing of state *)
     econstructor.
     crush.
@@ -2569,7 +2572,7 @@ Section CORRECTNESS.
           Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2.
   Proof.
     intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE.
-  
+
   #[local] Hint Resolve transl_ijumptable_correct : htlproof.*)
 
   Lemma transl_ireturn_correct:
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index 265b8f7..165fa91 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -120,11 +120,15 @@ Ltac monadInv H :=
     ((progress simpl in H) || unfold F in H); monadInv1 H
   end.
 
-(** * Relational specification of the translation *)
+(*|
+===========================================
+Relational specification of the translation
+===========================================
 
-(** We now define inductive predicates that characterise the fact that the
+We now define inductive predicates that characterise the fact that the
 statemachine that is created by the translation contains the correct
-translations for each of the elements *)
+translations for each of the elements.
+|*)
 
 Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
 | tr_instr_Inop :
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 1879205..2516109 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -30,10 +30,14 @@ Require Import vericert.bourdoncle.Bourdoncle.
 
 Parameter build_bourdoncle : function -> (bourdoncle * PMap.t N).
 
-(** * 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.  *)
+(*|
+=============
+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.
+|*)
 
 Definition combine_pred (p: pred_op) (optp: option pred_op) :=
   match optp with
diff --git a/src/hls/RICtransf.v b/src/hls/RICtransf.v
index d6e926b..643a3a7 100644
--- a/src/hls/RICtransf.v
+++ b/src/hls/RICtransf.v
@@ -27,12 +27,16 @@ Require Import vericert.hls.RTLBlockInstr.
 Require Import vericert.hls.RTLPar.
 Require Import vericert.hls.Predicate.
 
-(** * Reverse If-Conversion
+(*|
+=====================
+Reverse If-Conversion
+=====================
 
-This transformation takes a scheduling RTLPar block and removes any predicates from it.  It can then
-be trivially transformed into linear code again.  It works by iteratively selecting a predicate,
-then creating a branch based on it and placing subsequent instructions in one branch or the other.
-*)
+This transformation takes a scheduling RTLPar block and removes any predicates
+from it.  It can then be trivially transformed into linear code again.  It works
+by iteratively selecting a predicate, then creating a branch based on it and
+placing subsequent instructions in one branch or the other.
+|*)
 
 Fixpoint existsb_val {A B} (f: A -> option B) (l : list A) : option B :=
   match l with
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index 98e032b..ecd7561 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblock-main][rtlblock-main]] *)
 Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Events.
@@ -31,6 +30,12 @@ Require Import compcert.verilog.Op.
 
 Require Import vericert.hls.RTLBlockInstr.
 
+(*|
+========
+RTLBlock
+========
+|*)
+
 Definition bb := list instr.
 
 Definition bblock := @bblock bb.
@@ -43,16 +48,30 @@ Definition stackframe := @stackframe bb.
 Definition state := @state bb.
 
 Definition genv := @genv bb.
-(* rtlblock-main ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblock-semantics][rtlblock-semantics]] *)
+(*|
+Semantics
+=========
+
+We first describe the semantics by assuming a global program environment with
+type ~genv~ which was declared earlier.
+|*)
+
 Section RELSEM.
 
   Context (ge: genv).
-(* rtlblock-semantics ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::#step_instr_list][rtlblock-step_instr_list]] *)
-  Inductive step_instr_list: val -> instr_state -> list instr -> instr_state -> Prop :=
+(*|
+Instruction list step
+---------------------
+
+The ``step_instr_list`` definition describes the execution of a list of
+instructions in one big step, inductively traversing the list of instructions
+and applying the ``step_instr``.
+|*)
+
+  Inductive step_instr_list:
+    val -> instr_state -> list instr -> instr_state -> Prop :=
   | exec_RBcons:
     forall state i state' state'' instrs sp,
       step_instr ge sp state i state' ->
@@ -61,14 +80,21 @@ Section RELSEM.
   | exec_RBnil:
     forall state sp,
       step_instr_list sp state nil state.
-(* rtlblock-step_instr_list ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::#rtlblock-step][rtlblock-step]] *)
+(*|
+Top-level step
+--------------
+
+The step function itself then uses this big step of the list of instructions to
+then show a transition from basic block to basic block.
+|*)
+
   Variant step: state -> trace -> state -> Prop :=
   | exec_bblock:
     forall s f sp pc rs rs' m m' t s' bb pr pr',
       f.(fn_code)!pc = Some bb ->
-      step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') ->
+      step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body)
+                         (mk_instr_state rs' pr' m') ->
       step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' ->
       step (State s f sp pc rs pr m) t s'
   | exec_function_internal:
@@ -90,9 +116,7 @@ Section RELSEM.
     forall res f sp pc rs s vres m pr,
       step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m)
            E0 (State s f sp pc (rs#res <- vres) pr m).
-(* rtlblock-step ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::#rtlblock-step][rtlblock-rest]] *)
 End RELSEM.
 
 Inductive initial_state (p: program): state -> Prop :=
@@ -110,4 +134,3 @@ Inductive final_state: state -> int -> Prop :=
 
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
-(* rtlblock-rest ends here *)
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index bd40516..d23850a 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-imports][rtlblockinstr-imports]] *)
 Require Import Coq.micromega.Lia.
 
 Require Import compcert.backend.Registers.
@@ -31,20 +30,47 @@ Require Import compcert.verilog.Op.
 
 Require Import Predicate.
 Require Import Vericertlib.
-(* rtlblockinstr-imports ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-instr-def][rtlblockinstr-instr-def]] *)
 Definition node := positive.
 
+(*|
+=============
+RTLBlockInstr
+=============
+
+These instructions are used for ``RTLBlock`` and ``RTLPar``, so that they have
+consistent instructions, which greatly simplifies the proofs, as they will by
+default have the same instruction syntax and semantics.  The only changes are
+therefore at the top-level of the instructions.
+
+Instruction Definition
+======================
+
+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``).
+|*)
+
 Inductive instr : Type :=
 | RBnop : instr
-| RBop : option pred_op -> operation -> list reg -> reg -> instr
-| RBload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
-| RBstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
-| RBsetpred : option pred_op -> condition -> list reg -> predicate -> instr.
-(* rtlblockinstr-instr-def ends here *)
+| RBop :
+  option pred_op -> operation -> list reg -> reg -> instr
+| RBload :
+  option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
+| RBstore :
+  option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
+| RBsetpred :
+  option pred_op -> condition -> list reg -> predicate -> instr.
+
+(*|
+Control-Flow Instruction Definition
+===================================
+
+These are the instructions that count as control-flow, and will be placed at the
+end of the basic blocks.
+|*)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-cf-instr-def][rtlblockinstr-cf-instr-def]] *)
 Inductive cf_instr : Type :=
 | RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr
 | RBtailcall : signature -> reg + ident -> list reg -> cf_instr
@@ -55,9 +81,12 @@ Inductive cf_instr : Type :=
 | RBreturn : option reg -> cf_instr
 | RBgoto : node -> cf_instr
 | RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr.
-(* rtlblockinstr-cf-instr-def ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-helpers][rtlblockinstr-helpers]] *)
+(*|
+Helper Functions
+================
+|*)
+
 Fixpoint successors_instr (i : cf_instr) : list node :=
   match i with
   | RBcall sig ros args res s => s :: nil
@@ -67,7 +96,8 @@ Fixpoint successors_instr (i : cf_instr) : list node :=
   | RBjumptable arg tbl => tbl
   | RBreturn optarg => nil
   | RBgoto n => n :: nil
-  | RBpred_cf p c1 c2 => concat (successors_instr c1 :: successors_instr c2 :: nil)
+  | RBpred_cf p c1 c2 =>
+      concat (successors_instr c1 :: successors_instr c2 :: nil)
   end.
 
 Definition max_reg_instr (m: positive) (i: instr) :=
@@ -136,7 +166,8 @@ Lemma eval_predf_pr_equiv :
     eval_predf ps p = eval_predf ps' p.
 Proof.
   induction p; simplify; auto;
-    try (unfold eval_predf; simplify; repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto);
+    try (unfold eval_predf; simplify;
+         repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto);
   [repeat rewrite eval_predf_Pand|repeat rewrite eval_predf_Por];
   erewrite IHp1; try eassumption; erewrite IHp2; eauto.
 Qed.
@@ -146,17 +177,30 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
   | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs)
   | _, _ => Regmap.init Vundef
   end.
-(* rtlblockinstr-helpers ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-instr-state][rtlblockinstr-instr-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.
+|*)
+
 Record instr_state := mk_instr_state {
   is_rs: regset;
   is_ps: predset;
   is_mem: mem;
 }.
-(* rtlblockinstr-instr-state ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-type-def][rtlblockinstr-type-def]] *)
+(*|
+Top-Level Type Definitions
+==========================
+|*)
+
 Section DEFINITION.
 
   Context {bblock_body: Type}.
@@ -193,11 +237,17 @@ Section DEFINITION.
              (sp: val)             (**r stack pointer in calling function *)
              (pc: node)            (**r program point in calling function *)
              (rs: regset)          (**r register state in calling function *)
-             (pr: predset),        (**r predicate state of the calling function *)
+             (pr: predset),        (**r predicate state of the calling
+                                        function *)
       stackframe.
-(* rtlblockinstr-type-def ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::#state][rtlblockinstr-state]] *)
+(*|
+State Definition
+----------------
+
+Definition of the ``state`` type, which is used by the ``step`` functions.
+|*)
+
   Variant state : Type :=
   | State:
       forall (stack: list stackframe) (**r call stack *)
@@ -219,13 +269,14 @@ Section DEFINITION.
              (v: val)                 (**r return value for the call *)
              (m: mem),                (**r memory state *)
       state.
-(* rtlblockinstr-state ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::#state][rtlblockinstr-state]] *)
 End DEFINITION.
-(* rtlblockinstr-state ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-semantics][rtlblockinstr-semantics]] *)
+(*|
+Semantics
+=========
+|*)
+
 Section RELSEM.
 
   Context {bblock_body : Type}.
@@ -245,7 +296,8 @@ Section RELSEM.
       end
     end.
 
-  Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
+  Inductive eval_pred:
+    option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
   | eval_pred_true:
       forall i i' p,
       eval_predf (is_ps i) p = true ->
@@ -256,9 +308,7 @@ Section RELSEM.
       eval_pred (Some p) i i' i
   | eval_pred_none:
       forall i i', eval_pred None i i' i.
-(* rtlblockinstr-semantics ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::#step_instr][rtlblockinstr-step_instr]] *)
   Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop :=
   | exec_RBnop:
       forall sp ist,
@@ -266,28 +316,33 @@ Section RELSEM.
   | exec_RBop:
       forall op v res args rs m sp p ist pr,
         eval_operation ge sp op rs##args m = Some v ->
-        eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#res <- v) pr m) ist ->
+        eval_pred p (mk_instr_state rs pr m)
+                    (mk_instr_state (rs#res <- v) pr m) ist ->
         step_instr sp (mk_instr_state rs pr m) (RBop p op args res) ist
   | exec_RBload:
       forall addr rs args a chunk m v dst sp p pr ist,
         eval_addressing ge sp addr rs##args = Some a ->
         Mem.loadv chunk m a = Some v ->
-        eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#dst <- v) pr m) ist ->
-        step_instr sp (mk_instr_state rs pr m) (RBload p chunk addr args dst) ist
+        eval_pred p (mk_instr_state rs pr m)
+                    (mk_instr_state (rs#dst <- v) pr m) ist ->
+        step_instr sp (mk_instr_state rs pr m)
+                      (RBload p chunk addr args dst) ist
   | exec_RBstore:
       forall addr rs args a chunk m src m' sp p pr ist,
         eval_addressing ge sp addr rs##args = Some a ->
         Mem.storev chunk m a rs#src = Some m' ->
-        eval_pred p (mk_instr_state rs pr m) (mk_instr_state rs pr m') ist ->
-        step_instr sp (mk_instr_state rs pr m) (RBstore p chunk addr args src) ist
+        eval_pred p (mk_instr_state rs pr m)
+                    (mk_instr_state rs pr m') ist ->
+        step_instr sp (mk_instr_state rs pr m)
+                      (RBstore p chunk addr args src) ist
   | exec_RBsetpred:
       forall sp rs pr m p c b args p' ist,
       Op.eval_condition c rs##args m = Some b ->
-      eval_pred p' (mk_instr_state rs pr m) (mk_instr_state rs (pr#p <- b) m) ist ->
-      step_instr sp (mk_instr_state rs pr m) (RBsetpred p' c args p) ist.
-(* rtlblockinstr-step_instr ends here *)
+      eval_pred p' (mk_instr_state rs pr m)
+                   (mk_instr_state rs (pr#p <- b) m) ist ->
+      step_instr sp (mk_instr_state rs pr m)
+                    (RBsetpred p' c args p) ist.
 
-(* [[file:../../docs/scheduler-languages.org::#step_cf_instr][rtlblockinstr-step_cf_instr]] *)
   Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop :=
   | exec_RBcall:
     forall s f sp rs m res fd ros sig args pc pc' pr,
@@ -300,7 +355,8 @@ Section RELSEM.
       find_function ros rs = Some fd ->
       funsig fd = sig ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (RBtailcall sig ros args)
+      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m)
+                    (RBtailcall sig ros args)
         E0 (Callstate s fd rs##args m')
   | exec_RBbuiltin:
       forall s f sp rs m ef args res pc' vargs t vres m' pc pr,
@@ -327,13 +383,13 @@ Section RELSEM.
         E0 (Returnstate s (regmap_optget or Vundef rs) m')
   | exec_RBgoto:
       forall s f sp pc rs pr m pc',
-      step_cf_instr (State s f sp pc rs pr m) (RBgoto pc') E0 (State s f sp pc' rs pr m)
+      step_cf_instr (State s f sp pc rs pr m) (RBgoto pc') E0
+                    (State s f sp pc' rs pr m)
   | exec_RBpred_cf:
       forall s f sp pc rs pr m cf1 cf2 st' p t,
-      step_cf_instr (State s f sp pc rs pr m) (if eval_predf pr p then cf1 else cf2) t st' ->
-      step_cf_instr (State s f sp pc rs pr m) (RBpred_cf p cf1 cf2) t st'.
-(* rtlblockinstr-step_cf_instr ends here *)
+      step_cf_instr (State s f sp pc rs pr m)
+                    (if eval_predf pr p then cf1 else cf2) t st' ->
+      step_cf_instr (State s f sp pc rs pr m)
+                    (RBpred_cf p cf1 cf2) t st'.
 
-(* [[file:../../docs/scheduler-languages.org::#step_cf_instr][rtlblockinstr-end_RELSEM]] *)
 End RELSEM.
-(* rtlblockinstr-end_RELSEM ends here *)
diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v
index beca0ea..5d7376d 100644
--- a/src/hls/RTLBlockgen.v
+++ b/src/hls/RTLBlockgen.v
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(* [[file:../../docs/basic-block-generation.org::rtlblockgen-imports][rtlblockgen-imports]] *)
 Require compcert.backend.RTL.
 Require Import compcert.common.AST.
 Require Import compcert.lib.Maps.
@@ -28,7 +27,6 @@ Require Import vericert.hls.RTLBlockInstr.
 Require Import vericert.hls.RTLBlock.
 
 #[local] Open Scope positive.
-(* rtlblockgen-imports ends here *)
 
 Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}.
 Proof.
@@ -148,15 +146,19 @@ Defined.
 Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool :=
   if eqd a b then true else false.
 
-(* [[file:../../docs/basic-block-generation.org::rtlblockgen-main][rtlblockgen-main]] *)
 Parameter partition : RTL.function -> Errors.res function.
 
-(** [find_block max nodes index]: Does not need to be sorted, because we use filter and the max fold
-    function to find the desired element. *)
+(*|
+``find_block max nodes index``: Does not need to be sorted, because we use
+filter and the max fold function to find the desired element.
+
+    .. coq::
+|*)
+
 Definition find_block (max: positive) (nodes: list positive) (index: positive) : positive :=
   List.fold_right Pos.min max (List.filter (fun x => (index <=? x)) nodes).
 
-(*Compute find_block (2::94::28::40::19::nil) 40.*)
+(*Compute find_block 100 (2::94::48::39::19::nil) 40.*)
 
 Definition check_instr (n: positive) (istr: RTL.instruction) (istr': instr) :=
   match istr, istr' with
@@ -287,4 +289,3 @@ Definition transl_fundef := transf_partial_fundef transl_function.
 
 Definition transl_program : RTL.program -> Errors.res program :=
   transform_partial_program transl_fundef.
-(* rtlblockgen-main ends here *)
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v
index d51e5d4..4568185 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -16,25 +16,47 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(* [[file:../../docs/basic-block-generation.org::rtlblockgenproof-imports][rtlblockgenproof-imports]] *)
 Require compcert.backend.RTL.
 Require Import compcert.common.AST.
 Require Import compcert.lib.Maps.
+Require Import compcert.common.Errors.
 
+Require Import vericert.hls.RTLBlockInstr.
 Require Import vericert.hls.RTLBlock.
 Require Import vericert.hls.RTLBlockgen.
-(* rtlblockgenproof-imports ends here *)
 
-(* [[file:../../docs/basic-block-generation.org::rtlblockgenproof-match-states][rtlblockgenproof-match-states]] *)
+(*|
+Defining a find block specification
+-----------------------------------
+
+Basically, it should be able to find the location of the block without using the
+``find_block`` function, so that this is more useful for the proofs.  There are
+various different types of options that could come up though:
+
+1. The instruction is a standard instruction present inside of a basic block.
+2. The instruction is a standard instruction which ends with a ``goto``.
+3. The instruction is a control-flow instruction.
+
+For case number 1, there should exist a value in the list of instructions, such
+that the instructions match exactly, and the indices match as well.  In the
+original code, this instruction must have been going from the current node to
+the node - 1.  For case number 2, there should be an instruction at the right
+index again, however, this time there will also be a ``goto`` instruction in the
+control-flow part of the basic block.
+|*)
+
+(*Definition find_block_spec (c1: RTL.code) (c2: code) :=
+  forall x i,
+    c1 ! x = Some i ->
+    exists y li, c2 ! y = Some li /\ nth_error li.(bb_body) ((Pos.to_nat y) - (Pos.to_nat x))%nat = Some i.
+
 Inductive match_states : RTL.state -> RTLBlock.state -> Prop :=
 | match_state :
   forall stk f tf sp pc rs m
          (TF: transl_function f = OK tf),
-  match_states (RTL.State stk f sp pc rs m)
-               (RTLBlock.State stk tf sp (find_block max n i) rs m).
-(* rtlblockgenproof-match-states ends here *)
+    match_states (RTL.State stk f sp pc rs m)
+                 (State stk tf sp (find_block max n i) rs m).
 
-(* [[file:../../docs/basic-block-generation.org::rtlblockgenproof-correctness][rtlblockgenproof-correctness]] *)
 Section CORRECTNESS.
 
   Context (prog : RTL.program).
@@ -49,4 +71,4 @@ Section CORRECTNESS.
     apply senv_preserved.
 
 End CORRECTNESS.
-(* rtlblockgenproof-correctness ends here *)
+*)
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index f380d19..e0f657c 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlpar-main][rtlpar-main]] *)
 Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Events.
@@ -47,15 +46,16 @@ Section RELSEM.
 
   Context (ge: genv).
 
-  Inductive step_instr_list: val -> instr_state -> list instr -> instr_state -> Prop :=
-    | exec_RBcons:
-        forall state i state' state'' instrs sp,
-        step_instr ge sp state i state' ->
-        step_instr_list sp state' instrs state'' ->
-        step_instr_list sp state (i :: instrs) state''
-    | exec_RBnil:
-        forall state sp,
-        step_instr_list sp state nil state.
+  Inductive step_instr_list:
+    val -> instr_state -> list instr -> instr_state -> Prop :=
+  | exec_RBcons:
+    forall state i state' state'' instrs sp,
+      step_instr ge sp state i state' ->
+      step_instr_list sp state' instrs state'' ->
+      step_instr_list sp state (i :: instrs) state''
+  | exec_RBnil:
+    forall state sp,
+      step_instr_list sp state nil state.
 
   Inductive step_instr_seq (sp : val)
     : instr_state -> list (list instr) -> instr_state -> Prop :=
@@ -83,7 +83,8 @@ Section RELSEM.
   | exec_bblock:
     forall s f sp pc rs rs' m m' t s' bb pr pr',
       f.(fn_code)!pc = Some bb ->
-      step_instr_block sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') ->
+      step_instr_block sp (mk_instr_state rs pr m) bb.(bb_body)
+                          (mk_instr_state rs' pr' m') ->
       step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' ->
       step (State s f sp pc rs pr m) t s'
   | exec_function_internal:
@@ -126,7 +127,11 @@ Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
 Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) :=
-  let max_body := fold_left (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) bb.(bb_body) m in
+  let max_body :=
+    fold_left
+      (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x)
+      bb.(bb_body) m
+  in
   max_reg_cfi max_body bb.(bb_exit).
 
 Definition max_reg_function (f: function) :=
@@ -135,8 +140,9 @@ Definition max_reg_function (f: function) :=
     (fold_left Pos.max f.(fn_params) 1%positive).
 
 Definition max_pc_function (f: function) : positive :=
-  PTree.fold (fun m pc i => (Pos.max m
-                                     (pc + match Zlength i.(bb_body)
-                                           with Z.pos p => p | _ => 1 end))%positive)
-             f.(fn_code) 1%positive.
-(* rtlpar-main ends here *)
+  PTree.fold
+    (fun m pc i =>
+       (Pos.max m
+                (pc + match Zlength i.(bb_body)
+                      with Z.pos p => p | _ => 1 end))%positive)
+    f.(fn_code) 1%positive.
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 31ea51f..d425049 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(* [[file:../../docs/scheduler.org::rtlpargen-main][rtlpargen-main]] *)
 Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Globalenvs.
@@ -38,10 +37,22 @@ Import NE.NonEmptyNotation.
 #[local] Open Scope positive.
 #[local] Open Scope forest.
 #[local] Open Scope pred_op.
-(* rtlpargen-main ends here *)
 
-(* [[file:../../docs/scheduler.org::rtlpargen-generation][rtlpargen-generation]] *)
-Fixpoint list_translation (l : list reg) (f : forest) {struct l} : list pred_expr :=
+(*|
+=========
+RTLPargen
+=========
+
+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.
+|*)
+
+Fixpoint list_translation (l : list reg) (f : forest) {struct l}
+  : list pred_expr :=
   match l with
   | nil => nil
   | i :: l => (f # (Reg i)) :: (list_translation l f)
@@ -65,7 +76,8 @@ Definition merge'' x :=
   | ((a, e), (b, el)) => (merge''' a b, Econs e el)
   end.
 
-Definition map_pred_op {A B} (pf: option pred_op * (A -> B)) (pa: option pred_op * A): option pred_op * B :=
+Definition map_pred_op {A B} (pf: option pred_op * (A -> B))
+           (pa: option pred_op * A): option pred_op * B :=
   match pa, pf with
   | (p, a), (p', f) => (merge''' p p', f a)
   end.
@@ -74,8 +86,8 @@ Definition predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) :=
   NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end)
          (NE.non_empty_prod p1 p2).
 
-Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A): predicated B :=
-  NE.map (fun x => (fst x, f (snd x))) p.
+Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A)
+  : predicated B := NE.map (fun x => (fst x, f (snd x))) p.
 
 (*map (fun x => (fst x, Econs (snd x) Enil)) pel*)
 Definition merge' (pel: pred_expr) (tpel: predicated expression_list) :=
@@ -87,16 +99,20 @@ Fixpoint merge (pel: list pred_expr): predicated expression_list :=
   | a :: b => merge' a (merge b)
   end.
 
-Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A): predicated B :=
+Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A)
+  : predicated B :=
   predicated_map (fun x => (fst x) (snd x)) (predicated_prod pf pa).
 
-Definition predicated_apply1 {A B} (pf: predicated (A -> B)) (pa: A): predicated B :=
+Definition predicated_apply1 {A B} (pf: predicated (A -> B)) (pa: A)
+  : predicated B :=
   NE.map (fun x => (fst x, (snd x) pa)) pf.
 
-Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A) (pb: B): predicated C :=
+Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A)
+           (pb: B): predicated C :=
   NE.map (fun x => (fst x, (snd x) pa pb)) pf.
 
-Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D)) (pa: A) (pb: B) (pc: C): predicated D :=
+Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D))
+           (pa: A) (pb: B) (pc: C): predicated D :=
   NE.map (fun x => (fst x, (snd x) pa pb pc)) pf.
 
 Definition predicated_from_opt {A: Type} (p: option pred_op) (a: A) :=
@@ -133,9 +149,23 @@ 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).
-(* rtlpargen-generation ends here *)
 
-(* [[file:../../docs/scheduler.org::#update-function][rtlpargen-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 problem is that predicates need to be merged
+as well, so that:
+
+1. The predicates are *independent*.
+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.
+|*)
+
 Definition update (f : forest) (i : instr) : forest :=
   match i with
   | RBnop => f
@@ -149,7 +179,8 @@ Definition update (f : forest) (i : instr) : forest :=
       (app_predicated p
          (f # (Reg r))
          (map_predicated
-            (map_predicated (pred_ret (Eload chunk addr)) (merge (list_translation rl f)))
+            (map_predicated (pred_ret (Eload chunk addr))
+                            (merge (list_translation rl f)))
             (f # Mem)))
   | RBstore p chunk addr rl r =>
     f # Mem <-
@@ -157,30 +188,45 @@ Definition update (f : forest) (i : instr) : forest :=
          (f # Mem)
          (map_predicated
             (map_predicated
-               (predicated_apply2 (map_predicated (pred_ret Estore) (f # (Reg r))) chunk addr)
+               (predicated_apply2 (map_predicated (pred_ret Estore)
+                                                  (f # (Reg r))) chunk addr)
                (merge (list_translation rl f))) (f # Mem)))
   | RBsetpred p' c args p =>
     f # (Pred p) <-
     (app_predicated p'
        (f # (Pred p))
-       (map_predicated (pred_ret (Esetpred c)) (merge (list_translation args f))))
+       (map_predicated (pred_ret (Esetpred c))
+                       (merge (list_translation args f))))
   end.
-(* rtlpargen-update-function ends here *)
 
-(* [[file:../../docs/scheduler.org::#update-function][rtlpargen-abstract-seq]] *)
+(*|
+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.
+|*)
+
 Fixpoint abstract_sequence (f : forest) (b : list instr) : forest :=
   match b with
   | nil => f
   | i :: l => abstract_sequence (update f i) l
   end.
-(* rtlpargen-abstract-seq ends here *)
 
-(* [[file:../../docs/scheduler.org::#update-function][rtlpargen-check-functions]] *)
+(*|
+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.
-(* rtlpargen-check-functions ends here *)
 
-(* [[file:../../docs/scheduler.org::#update-function][rtlpargen-top-check-functions]] *)
+(*|
+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
   | nil =>
@@ -219,12 +265,16 @@ Lemma check_scheduled_trees_correct2:
     PTree.get x f1 = None ->
     PTree.get x f2 = None.
 Proof. solve_scheduled_trees_correct. Qed.
-(* rtlpargen-top-check-functions ends here *)
 
-(* [[file:../../docs/scheduler.org::rtlpargen-top-level-functions][rtlpargen-top-level-functions]] *)
+(*|
+Top-level Functions
+===================
+|*)
+
 Parameter schedule : RTLBlock.function -> RTLPar.function.
 
-Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function :=
+Definition transl_function (f: RTLBlock.function)
+  : Errors.res RTLPar.function :=
   let tfcode := fn_code (schedule f) in
   if check_scheduled_trees f.(fn_code) tfcode then
     Errors.OK (mkfunction f.(fn_sig)
@@ -233,10 +283,10 @@ Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function :
                           tfcode
                           f.(fn_entrypoint))
   else
-    Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent.").
+    Errors.Error
+      (Errors.msg "RTLPargen: Could not prove the blocks equivalent.").
 
 Definition transl_fundef := transf_partial_fundef transl_function.
 
 Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program :=
   transform_partial_program transl_fundef p.
-(* rtlpargen-top-level-functions ends here *)
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index 6d61572..4e88b13 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(* [[file:../../docs/scheduler.org::rtlpargenproof-imports][rtlpargenproof-imports]] *)
 Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Errors.
@@ -37,9 +36,18 @@ Require Import vericert.hls.Abstr.
 #[local] Open Scope positive.
 #[local] Open Scope forest.
 #[local] Open Scope pred_op.
-(* rtlpargenproof-imports ends here *)
 
-(* [[file:../../docs/scheduler.org::rtlpargenproof-main][rtlpargenproof-main]] *)
+(*|
+==============
+RTLPargenproof
+==============
+
+RTLBlock to abstract translation
+================================
+
+Correctness of translation from RTLBlock to the abstract interpretation language.
+|*)
+
 (*Definition is_regs i := match i with mk_instr_state rs _ => rs end.
 Definition is_mem i := match i with mk_instr_state _ m => m end.
 
@@ -1134,4 +1142,3 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
   Qed.
 
 End CORRECTNESS.
-(* rtlpargenproof-main ends here *)
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 3a5351e..70395e7 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(* [[file:../../docs/scheduler.org::scheduler-main][scheduler-main]] *)
 open Printf
 open Clflags
 open Camlcoq
@@ -882,4 +881,3 @@ let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function =
     fn_code = scheduled (*List.fold_left (add_to_tree scheduled) PTree.empty reachable*);
     fn_entrypoint = f.fn_entrypoint
   }
-(* scheduler-main ends here *)
diff --git a/src/hls/ValueInt.v b/src/hls/ValueInt.v
index e434abc..06b5630 100644
--- a/src/hls/ValueInt.v
+++ b/src/hls/ValueInt.v
@@ -22,22 +22,31 @@ From compcert Require Import lib.Integers common.Values.
 From vericert Require Import Vericertlib.
 (* end hide *)
 
-(** * Value
+(*|
+=====
+Value
+=====
 
-A [value] is a bitvector with a specific size. We are using the implementation
+A ``value`` is a bitvector with a specific size. We are using the implementation
 of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse.
-However, we need to wrap it with an [Inductive] so that we can specify and match
-on the size of the [value]. This is necessary so that we can easily store
-[value]s of different sizes in a list or in a map.
+However, we need to wrap it with an ``Inductive`` so that we can specify and
+match on the size of the ``value``. This is necessary so that we can easily
+store ``value`` of different sizes in a list or in a map.
 
-Using the default [word], this would not be possible, as the size is part of the type. *)
+Using the default ``word``, this would not be possible, as the size is part of
+the type.
+|*)
 
 Definition value : Type := int.
 
-(** ** Value conversions
+(*|
+Value conversions
+=================
 
-Various conversions to different number types such as [N], [Z], [positive] and
-[int], where the last one is a theory of integers of powers of 2 in CompCert. *)
+Various conversions to different number types such as ``N``, ``Z``, ``positive``
+and ``int``, where the last one is a theory of integers of powers of 2 in
+CompCert.
+|*)
 
 Definition valueToNat (v : value) : nat :=
   Z.to_nat (Int.unsigned v).
@@ -83,10 +92,12 @@ Definition valToValue (v : Values.val) : option value :=
   | _ => None
   end.
 
-(** Convert a [value] to a [bool], so that choices can be made based on the
-result. This is also because comparison operators will give back [value] instead
-of [bool], so if they are in a condition, they will have to be converted before
-they can be used. *)
+(*|
+Convert a ``value`` to a ``bool``, so that choices can be made based on the
+result. This is also because comparison operators will give back ``value``
+instead of ``bool``, so if they are in a condition, they will have to be
+converted before they can be used.
+|*)
 
 Definition valueToBool (v : value) : bool :=
   if Z.eqb (uvalueToZ v) 0 then false else true.
@@ -94,7 +105,10 @@ Definition valueToBool (v : value) : bool :=
 Definition boolToValue (b : bool) : value :=
   natToValue (if b then 1 else 0).
 
-(** ** Arithmetic operations *)
+(*|
+Arithmetic operations
+---------------------
+|*)
 
 Inductive val_value_lessdef: val -> value -> Prop :=
 | val_value_lessdef_int:
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index 7561f77..72140cd 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -142,23 +142,28 @@ 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.
+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 [+]) *)
@@ -186,13 +191,19 @@ Inductive binop : Type :=
 | Vshru : 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
@@ -207,7 +218,10 @@ Inductive expr : Type :=
 Definition posToExpr (p : positive) : expr :=
   Vlit (posToValue p).
 
-(** *** Statements *)
+(*|
+Statements
+----------
+|*)
 
 Inductive stmnt : Type :=
 | Vskip : stmnt
@@ -220,13 +234,17 @@ 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
@@ -234,11 +252,15 @@ 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
@@ -255,15 +277,17 @@ 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.
-- [mod_clk] The clock that controls the computation in the module.
-- [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_start: If set, starts the computations in the module.
+:mod_reset: If set, reset the state in the module.
+:mod_clk: The clock that controls the computation in the module.
+: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.
+|*)
 
 Record module : Type := mkmodule {
   mod_start : reg;
@@ -271,7 +295,8 @@ Record module : Type := mkmodule {
   mod_clk : reg;
   mod_finish : reg;
   mod_return : reg;
-  mod_st : reg; (**r Variable that defines the current state, it should be internal. *)
+  mod_st : reg; (**r Variable that defines the current state,
+                     it should be internal. *)
   mod_stk : reg;
   mod_stk_len : nat;
   mod_args : list reg;
@@ -283,33 +308,39 @@ 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:
+The ``state`` contains the following items:
 
-- 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.
-- A contiunation ([cont]) which defines what to do next.  The option is to
-  either evaluate another module item or go to the next clock cycle.  Finally
-  it could also end if the finish flag of the module goes high.
+- 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.
+- A contiunation (``cont``) which defines what to do next.  The option is to
+  either evaluate another module item or go to the next clock cycle.  Finally it
+  could also end if the finish flag of the module goes high.
 - Association list containing the blocking assignments made, or assignments made
   in previous clock cycles.
 - Nonblocking association list containing all the nonblocking assignments made
   in the current module.
 - The environment containing values for the input.
-- The program counter which determines the value for the state in this version of
-  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.  *)
+- The program counter which determines the value for the state in this version
+  of 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.
+|*)
 
 Inductive stackframe : Type :=
   Stackframe :
@@ -429,7 +460,9 @@ 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)