Start writing more documentation

.gitignore

@@ -2,3 +2,4 @@
 *.dat
 *.uo
 *.ui
+.HOLMK/*

README.md

 # Icing
 
-A new, nondeterministic floating-point source semantics and a proof-of-concept connection to the CakeML verified compiler.
+A new, nondeterministic floating-point source semantics and a proof-of-concept
\ No newline at end of file
+connection to the CakeML verified compiler.
+
+The development is known to compile with HOL4 running on commit
+`30c14988fa7ce031bc99f6828e07df9529e6c3a9`.
+
+The folder `cakeml` contains the CakeML verified compiler as a git submodule.
+To checkout the latest revision which compiles with Icing run
+
+    git submodule update --init cakeml
+
+Afterwards the `cakeml` folder should be up-to-date.
+
+To compile the development run `Holmake` after initializing the CakeML submodule.
+All of the files, apart from `CakeMLconnScript.sml` can be build without
+the CakeML compiler being initialized and do not depend on CakeML internals,
+however it is necessary to initialize the submodule because HOL4 wants to
+compile CakeML dependencies first.
\ No newline at end of file

SyntaxScript.sml

 (**
-  Formalization of the syntax of Flour
+  This file defines the syntax of Icing expressions and utility functions
+  computing sets of variables.
+  The syntax of Icing is described in section 2.1 of our CAV 2019 paper
 **)
 open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory;
 open valueTreesTheory;
@@ -8,12 +10,13 @@ open flourPreamble;
 
 val _ = new_theory "Syntax";
 
-(** Formal definition of the syntax defined in Figure 2 **)
+(** Formal definition of the syntax defined in Figure 1 **)
 val _ = Datatype `
   expr =
         (* Leaf nodes, constants and variables *)
           Wconst word64
         | Var string
+        (* Lists are lists of Icing expressions *)
         | List (expr list)
         (* Simple projection into lists *)
         | Ith num expr
@@ -24,9 +27,10 @@ val _ = Datatype `
         (* Control flow - let bindings and if-statements *)
         | Let string expr expr
         | Cond cexpr expr expr
-        (* Scoping, make all things below IEEE correct *)
+        (* Scoping, make all things below optimizable *)
         | Scope scope expr
-        (* Complex control-flow, to support limited recursion *)
+        (* List manipulating functions map and fold and their value tree
+           counterparts which are only used in the semantics *)
         | Map string expr expr
         | Mapvl string expr (valTree list)
         | Fold (string # string) expr expr expr
@@ -42,6 +46,12 @@ val _ = Datatype `
         (* boolean Scoping *)
         | Cscope scope cexpr`;
 
+(**
+  Functions to compute the free variables and the used variables of expressions.
+  Free variables are not let-bound, and not parameters of lambdas for fold and
+  map.
+  Used variables are free variables, let-bound variables and parameters of
+  lambdas **)
 val freeVarsExp_def =  tDefine
   "freeVarsExp"
   `(freeVarsExp (Wconst _) = {}) /\

patternProofsScript.sml

+(**
+  This file contains proofs about the matching and instantiation functions
+  defined in patternScript.sml
+  It also contains some compatibility lemmas for rwAllValTree, the value tree
+  rewriting function
+**)
+
 open SyntaxTheory patternTheory;
 
 open flourPreamble;

patternScript.sml

 (**
-  Formalization of the rewriting functions
-  from section 3.2 in the paper
-**)
+  Formalization of the pattern language and top-level matching and
+  application functions which are later used to define rewriting
+  The pattern language and rewriting are defined in section 2.2 of the CAV 2019
+  paper. Proofs about the pattern matching and instantiation are in
+  patternProofsScript.sml **)
 open SyntaxTheory valueTreesTheory;
 
 open flourPreamble;
@@ -11,7 +13,6 @@ val _ = new_theory "pattern";
 (**
   Inductive Datatype for our pattern language
   Must support matching on any expression, variables are used for patterns
-  Formal definition of the patterns from Figure 4
 **)
 val _ = Datatype `
   pat =
@@ -25,10 +26,9 @@ val _ = Datatype `
   | Cmp cmp pat pat
   | Scope scope pat;`
 
-(* Define a rewrite rule to be a pair of two patterns.
-  The left hand side is the pattern to match and the right hand side is the
-  returned value/ expression
-*)
+(* A rewrite rule is a pair of two patterns.
+  The left hand side is the pattern to match against
+  and the right hand side is the returned value/expression *)
 val _ = type_abbrev ("rw_rule", ``:pat # pat``);
 val _ = temp_type_abbrev ("val_subst", ``:num |-> valTree``);
 val _ = temp_type_abbrev ("exp_subst", ``:num |-> expr``);
@@ -229,10 +229,22 @@ val appExpr_def = Define `
       od) /\
     appCexpr _ _ = NONE`;
 
+(** Rewriting on value trees is done in the semantics by picking a path
+  that walks down the value tree structure and then applies the rewrite in place
+  if it matches **)
+
+(* Datatype for paths into a value tree. Here is the leaf node meaning that the
+  rewrite should be applied *)
 val _ = Datatype `
   path =
   | Left path | Right path | Center path | Here`;
 
+(* Function rwPathValTree b rw p v recurses through value tree v using path p
+  until p = Here or no further recursion is possible because of a mismatch.
+  In case of a mismatch the function simply returns None.
+  Flag b is used to track whether we have passed an `opt` annotation allowing
+  optimizations to be applied.
+  Only if b is true, and p = Here, the rewrite rw is applied. *)
 val rwPathValTree_def = Define `
   rwPathValTree F rw Here v = NONE /\
   rwPathValTree T rw Here v =
@@ -272,10 +284,14 @@ val rwPathValTree_def = Define `
     OPTION_MAP (\v. Cscope sc v) (rwPathCvalTree (sc = Opt \/ b) rw p v) /\
   rwPathCvalTree _ _ _ _ = NONE`;
 
+(* Datatype holding a single rewrite application in the form of a path into the
+  value tree and a number giving the index of the rewrite to be used *)
 val _ = Datatype `
   rewrite_app =
     | RewriteApp path num (* which rewrite rule *)`;
 
+(* rwAllValTree rwApps canOpt rws v applies all the rewrite_app's in rwApps to
+    value tree v using rwPathValTree *)
 val rwAllValTree_def = Define `
   rwAllValTree [] canOpt rws v = SOME v /\
   rwAllValTree ((RewriteApp p index)::rs) canOpt rws v =
@@ -296,6 +312,8 @@ val rwAllCvalTree_def = Define `
       | NONE => NONE
       | SOME v_new => rwAllCvalTree rs canOpt rws v_new)`;
 
+(* rewriteExp: Non-recursive, expression rewriting function applying all rewrites that match.
+  A non-matching rewrite is silently ignored *)
 val rewriteExp_def = Define `
   rewriteExp ([]:rw_rule list) (e:expr) = e /\
   rewriteExp ((lhs,rhs)::rwtl) e =

rewriteRulesProofsScript.sml

+(**
+  This file gives simulation proofs for each rewrite separately
+  For each rewrite we show that its syntactic application at the top-level
+  can be simulated by adding the rewrite to the set of rewrites allowed
+  for the semantics
+**)
 open SyntaxTheory CompilerTheory rewriteRulesTheory patternTheory
      patternProofsTheory SemanticsTheory;
 open CompilerTacticsLib;
@@ -65,6 +71,7 @@ Theorem ASSOCRULE_GEN_correct
   \\ Cases_on `cfg.canOpt` \\ fs[]
   \\ ignore_sem_rws_tac);
 
+(** Associativity theorems by instantiation **)
 val assoc_thms =
   List.map
   (fn (s,b) =>
@@ -117,6 +124,7 @@ Theorem COMMRULE_GEN_correct
   \\ Cases_on `cfg.canOpt` \\ fs[]
   \\ ignore_sem_rws_tac);
 
+(** Commutativity theorems by instantiation **)
 val comm_thms =
   List.map
   (fn (s,b) =>
@@ -135,6 +143,8 @@ Theorem PMDISTRIBRULE_cases
   (rpt strip_tac \\ Cases_on `e12` \\ EVAL_TAC \\ fs[]
   \\ TOP_CASE_TAC \\ fs[] \\ rveq \\ EVAL_TAC);
 
+(** Syntactic criterion to check that distributivity can be applied,
+  see section 4.3 of our CAV 2019 paper for a discussion *)
 val isVarDistr_def = Define `
   isVarDistr (e:expr) =
   case e of

rewriteRulesScript.sml

+(**
+  This file defines the rewrite rules used in the Icing compiler.
+  In the CAV 2019 paper the rewrites are defined in Table 1
+**)
+
 open SemanticsTheory patternTheory valueTreesTheory;
 
 open flourPreamble;
 
 val _ = new_theory "rewriteRules";
 
-(** Below we define some basic real-valued algebraic laws as rewrites **)
+(** Real-valued, algebraic laws as rewrites **)
 
 (** A generator for associativity rewrites **)
 val ASSOCRULE_GEN_def = Define `
@@ -12,9 +17,15 @@ val ASSOCRULE_GEN_def = Define `
     (Binop b (Var 0) (Binop b (Var 1) (Var 2)),
      Binop b (Binop b (Var 0) (Var 1)) (Var 2))`;
 
+(**
+  a + (b + c) -> (a + b) + c
+**)
 val PLUSASSOCRULE_def = Define `
   PLUSASSOCRULE = ASSOCRULE_GEN Plus`;
 
+(**
+  a * (b * c) -> (a * b) * c
+**)
 val MULTASSOCRULE_def = Define `
   MULTASSOCRULE = ASSOCRULE_GEN Mult`;
 
@@ -23,24 +34,38 @@ val COMMRULE_GEN_def = Define `
   COMMRULE_GEN (b:binop) =
   (Binop b (Var 0) (Var 1), Binop b (Var 1) (Var 0))`;
 
+(**
+  a + b -> b + a
+**)
 val PLUSCOMMRULE_def = Define `
   PLUSCOMMRULE = COMMRULE_GEN Plus`;
 
+(**
+  a * b -> b * a
+**)
 val MULTCOMMRULE_def = Define `
   MULTCOMMRULE = COMMRULE_GEN Mult`;
 
+(** Distributivity of +,*:
+  a * (b + c) -> a * b + a * c
+**)
 val PMDISTRIBRULE_def = Define `
   PMDISTRIBRULE =
     (Binop Mult (Var 0) (Binop Plus (Var 1) (Var 2)),
      Binop Plus (Binop Mult (Var 0) (Var 1)) (Binop Mult (Var 0) (Var 2)))`;
 
+(** Double negation:
+  - - a -> a
+**)
 val DNEGRULE_def = Define `
   DNEGRULE =
     (Unop Neg (Unop Neg (Var 0)), Var 0) `;
 
 (**  floating-point specific rewrites **)
 
-(** FMA introduction **)
+(** FMA introduction
+  a * b + c -> FMA (a,b,c)
+**)
 val FMARULE_def = Define `
   FMARULE =
     (Binop Plus (Binop Mult (pattern$Var 0) (Var 1)) (Var 2),
@@ -48,8 +73,8 @@ val FMARULE_def = Define `
 
 (** Rewrites assuming real-valued behavior for floating-point *)
 
-(** Removing NaN checks, this rewrite should only be applied with a side condition **)
-
+(** Removing NaN checks, this rewrite should only be applied with a rewrite
+    precondition **)
 val NONANCHECKRULE_def = Define `
   NONANCHECKRULE =
   ((Pred NaN (Var 0)), Bool F)`;

valueTreesScript.sml

 (**
-  Formalization of the value trees from the paper
+  This file defines the value trees datatype and some functions operating on it.
+  Value trees are described in Section 2.3 of our CAV 2019 paper
 **)
 open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory listTheory;
 open flourPreamble;
 
 val _ = new_theory "valueTrees";
 
+(** Define datatypes for operations once and reuse them also on syntax level **)
 val _ = Datatype `
   unop = Neg | Sqrt;
   binop = Plus | Minus | Mult | Div;
@@ -14,7 +16,7 @@ val _ = Datatype `
   pred = NaN;
   scope = Opt`;
 
-(** Formal definition of the value trees **)
+(** Formal definition of value trees **)
 val _ = Datatype `
   valTree = Wconst word64
             | UnVal unop valTree
@@ -31,7 +33,7 @@ val _ = Datatype `
           | Cval cvalTree
           | Lval (valTree list)`;
 
-(* Function tree2IEEE in the paper **)
+(* Function tree2IEEE in the CAV paper **)
 val tree2IEEE_def = Define `
   tree2IEEE (Wconst c) = c /\
   tree2IEEE (UnVal op v) =