Update documentation for Compiler.v

1 files changed, 84 insertions, 0 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index 8eeea6b..332d506 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -1,3 +1,7 @@
+(*|
+.. coq:: none
+|*)
+
 (*
  * Vericert: Verified high-level synthesis.
  * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
@@ -16,6 +20,22 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
+(*|
+==============
+Compiler Proof
+==============
+
+.. contents:: Table of Contents
+   :depth: 2
+
+This is the top-level module of the correctness proof and proves the final backwards simulation correct.
+
+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.
+|*)
+
 From vericert Require Import HTLgenproof.
 
 From compcert.common Require Import
@@ -58,6 +78,13 @@ From vericert Require
 
 From compcert Require Import Smallstep.
 
+(*|
+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``.
+|*)
+
 Parameter print_RTL: Z -> RTL.program -> unit.
 Parameter print_HTL: HTL.program -> unit.
 Parameter print_RTLBlock: RTLBlock.program -> unit.
@@ -72,11 +99,19 @@ 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.
+|*)
+
 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.
+|*)
+
 Lemma compose_print_identity:
   forall (A: Type) (x: res A) (f: A -> unit),
   x @@ print f = x.
@@ -84,6 +119,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.
+|*)
+
 Definition total_if {A: Type}
           (flag: unit -> bool) (f: A -> A) (prog: A) : A :=
   if flag tt then f prog else prog.
@@ -94,6 +133,13 @@ Definition partial_if {A: Type}
 
 Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.
 
+(*|
+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.
+|*)
+
 Definition transf_backend_opt (r : RTL.program) : res Verilog.program :=
   OK r
   @@@ Inlining.transf_program
@@ -124,6 +170,10 @@ Definition transf_backend (r : RTL.program) : res Verilog.program :=
    @@ print print_HTL
    @@ Veriloggen.transl_program.
 
+(*|
+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
   @@@ SimplExpr.transl_program
@@ -146,6 +196,10 @@ Definition transf_hls_opt (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_RTL 0)
   @@@ transf_backend_opt.
 
+(*|
+.. coq:: none
+|*)
+
 Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
   OK p
   @@@ SimplExpr.transl_program
@@ -174,6 +228,13 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ print print_HTL
    @@ Veriloggen.transl_program.
 
+(*|
+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.
+|*)
+
 Local Open Scope linking_scope.
 
 Definition CompCert's_passes :=
@@ -189,9 +250,17 @@ 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.
+|*)
+
 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.
+|*)
+
 Theorem transf_hls_match:
   forall p tp,
     transf_hls p = OK tp ->
@@ -278,6 +347,13 @@ Ltac DestructM :=
   apply Verilog.semantics_determinate.
 Qed.
 
+(*|
+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.
+|*)
+
 Theorem c_semantic_preservation:
   forall p tp,
   match_prog p tp ->
@@ -293,6 +369,10 @@ 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.
+|*)
+
 Theorem transf_c_program_correct:
   forall p tp,
   transf_hls p = OK tp ->
@@ -301,6 +381,10 @@ 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.
+|*)
+
 Theorem separate_transf_c_program_correct:
   forall c_units verilog_units c_program,
   nlist_forall2 (fun cu tcu => transf_hls cu = OK tcu) c_units verilog_units ->