Add 2 to 3 line comment to every file to explain where it is used and what it...

Add 2 to 3 line comment to every file to explain where it is used and what it contains. Add references to paper where possible

coq/ErrorBounds.v

 (**
 Proofs of general bounds on the error of arithmetic expressions.
 This shortens soundness proofs later.
+Bounds are explained in section 5, Deriving Computable Error Bounds
 **)
 Require Import Coq.Reals.Reals Coq.micromega.Psatz Interval.Interval_tactic.
 Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Expressions.

coq/ErrorValidation.v

 (**
    This file contains the coq implementation of the error bound validator as well as its soundness proof.
+   It is explained in section 5 of the paper.
+   The validator is used in the file CertificateChecker.v to build the complete checker.
  **)
 Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals Coq.Lists.List.
 Require Import Coq.micromega.Psatz Coq.Reals.Reals.

coq/Expressions.v

 (**
 Formalization of the base expression language for the daisy framework
+Required in all files, since we will always reason about expressions.
  **)
 Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith.
 Require Import Daisy.Infra.RealSimps Daisy.Infra.Abbrevs.

coq/IntervalArith.v

 (**
   Formalization of real valued interval arithmetic
+  Used in soundness proofs for error bound validator.
 **)
 Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
 Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RealSimps.

coq/IntervalArithQ.v

 (**
-  Formalization of real valued intv arithmetic
-  TODO: Package this into a class or module that depends only on proving the existence of basic operators instead
+  Formalization of rational valued interval arithmetic
+  Used in soundness proofs and computations of range validator.
 **)
 Require Import Coq.QArith.QArith Coq.QArith.Qminmax.
 Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RationalSimps.

coq/IntervalValidation.v

 (**
 Interval arithmetic checker and its soundness proof
+Explained in section 4 of the paper, used in CertificateChecker.v to build full checker,
 **)
 Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List.
 Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.

hol/ErrorBounds.hl

+(**
+   Proofs of general bounds on the error of arithmetic expressions.
+   This shortens soundness proofs later.
+   Bounds are explained in section 5, Deriving Computable Error Bounds
+**)
 needs "Infra/Abbrevs.hl";;
 needs "Infra/RealSimps.hl";;
 needs "Expressions.hl";;

hol/ErrorValidation.hl

 (**
    This file contains the HOL-Light implementation of the error bound validator as well as its soundness proof.
+   It is explained in section 5 of the paper.
+   The validator is used in the file CertificateChecker.hl to build the complete checker.
  **)
 needs "Infra/ExpressionAbbrevs.hl";;
 needs "IntervalValidation.hl";;

hol/Expressions.hl

 (**
    Formalization of the base expression language for the daisy framework
-**)
+   Required in all files, since we will always reason about expressions.
+ **)
 needs "Infra/tactics.hl";;
 needs "Infra/RealConstruction.hl";;
 needs "Infra/RealSimps.hl";;

hol/IntervalArith.hl

-(*
-  Basic Definitions of Interval Arithmetic, for all binary operators
-*)
+(**
+  Formalization of real valued interval arithmetic
+  Used in soundness proofs for error bound validator and range validator
+**)
 needs "Infra/tactics.hl";;
 needs "Infra/Abbrevs.hl";;
 needs "Infra/RealSimps.hl";;

hol/IntervalValidation.hl

+(**
+   Interval arithmetic checker and its soundness proof
+   Explained in section 4 of the paper, used in CertificateChecker.hl to build full checker,
+**)
 needs "Infra/tactics.hl";;
 needs "Infra/Abbrevs.hl";;
 needs "Expressions.hl";;