Update with comments

Author: HeikoBecker

icing/CakeMLtoFloVerLemsScript.sml

@@ -1,5 +1,7 @@
 (*
-  Lemmas for connection to FloVer
+  Lemmas for connection to FloVer,
+  the translation function is defined in CakeMLtoFloVerScript.sml, and the main
+  connection theorem in CakeMLtoFloVerProofsScript.sml
 *)
 (* HOL4 *)
 open machine_ieeeTheory realTheory realLib RealArith;

icing/CakeMLtoFloVerProofsScript.sml

@@ -1,5 +1,6 @@
 (*
-  Central theorem about connection to FloVer
+  Main connection theorem relating FloVer's roundoff error bound
+  to CakeML floating-point kernel executions
 *)
 (* HOL4 *)
 open machine_ieeeTheory realTheory realLib RealArith;

icing/CakeMLtoFloVerScript.sml

@@ -1,5 +1,5 @@
 (*
- Definition of translation to FloVer
+  Translation from CakeML floating-point kernels to FloVer input
 *)
 (* CakeML *)
 open compilerTheory;
@@ -264,190 +264,3 @@ Definition getError_def:
 End
 
 val _ = export_theory ();
-
-    (**
-Definition Eval_oracle_def:
-  Eval_oracle env exp P oracle =
-  ∀ refs.
-  ∃ res.
-End
-
-
-Theorem evaluate_const:
-  Eval env (App FpFromWord [Lit (Word64 w)]) ((=) (FP_WordTree (Fp_const w)))
-Proof
-  fs[ml_translatorTheory.Eval_def, ml_progTheory.eval_rel_def]
-  \\ EVAL_TAC \\ fs[]
-QED
-
-Theorem evaluate_var:
-  nsLookup env.v (Short x) = SOME fp ⇒
-  Eval env (Var (Short x)) ((=) fp)
-Proof
-  fs[ml_translatorTheory.Eval_def, ml_progTheory.eval_rel_def]
-  \\ EVAL_TAC \\ fs[]
-QED
-
-Theorem evaluate_bop:
-  Eval env e1 ((=) (FP_WordTree fp1)) ∧
-  Eval env e2 ((=) (FP_WordTree fp2)) ⇒
-  Eval env (App (FP_bop bop) [e1;e2]) ((=) (FP_WordTree (Fp_bop bop fpT1 fpT2)))
-Proof
-  rpt strip_tac
-  \\ simp [ml_translatorTheory.Eval_def, ml_progTheory.eval_rel_def]
-  \\ simp[terminationTheory.evaluate_def, astTheorsemanticPrimitivesTheoryy.getOpClass_def]
-  \\ EVAL_TAC \\ fs[]
-
-
-
-exception valError of string;
-
-fun translate t =
-  case free_vars t of
-  v::vs => raise valError "No free vars allowed"
-  | [] =>
-**)
-
-(** UNUSED:
-
-Definition isFloVerExps_def:
-  isFloVerExps [Var x] = T ∧
-  isFloVerExps [App op exps] =
-    (isFloVerExps exps  ∧
-    (case op of
-     | FP_bop _ => LENGTH exps = 2
-     | FP_uop FP_Neg => LENGTH exps = 1
-     | FP_top _ => LENGTH exps = 3
-     | _ =>  F)) ∧
-  isFloVerExps [e] = F ∧
-  isFloVerExps (e1::es) = (isFloVerExps [e1] ∧ isFloVerExps es)
-Termination
-  wf_rel_tac `measure exp6_size`
-End
-
-Definition isFloVerCmd_def:
-  isFloVerCmd (Let so e1 e2) =
-  (case so of
-   | SOME x => isFloVerExps [e1] ∧ isFloVerCmd e2
-   | NONE => F) ∧
-  isFloVerCmd (App op exps) = isFloVerExps [App op exps] ∧
-  isFloVerCmd (Var x) = T ∧
-  isFloVerCmd _ = F
-End
-
-Definition stripAssert_def:
-  stripAssert (Let NONE P body) =
-    (case P of
-    | App op [fN; P] =>
-      if (op = Opapp ∧ fN = Var (Long "Runtime" (Short "assert")))
-      then SOME (P, body)
-      else NONE
-    | _ => NONE) ∧
-  stripAssert _ = NONE
-End
-
-Definition prepareKernel_def:
-  prepareKernel exps =
-    case exps of
-    | NONE => NONE
-    | SOME exps =>
-      if (LENGTH exps ≠ 1)
-      then NONE
-      else
-        case exps of
-        | [(n1, n2, e)] =>
-        let
-          fN = stripNoOpt e;
-          (vars, body) = stripFuns fN in
-        do
-          (P, body) <- stripAssert body;
-          (* FIXME: should not need to strip noopt annotations here *)
-          return (n2::vars, P, stripNoOpt body);
-        od
-        | _ => NONE
-End
-
-(**
-  Function getInterval
-  Argument:
-    A single CakeML AST describing an interval constraint
-    The argument must have the shape (lo ≤ x) ∧ (x ≤ hi)
-  Returns:
-    The CakeML variable constraint by the interval, the lower bound,
-    the upper bound
-**)
-Definition getInterval_def:
-  getInterval (Log lop e1 e2) =
-    (if (lop <> And) then NONE
-    else
-      case e1 of
-      | App (FP_cmp FP_LessEqual) [c1; var1] =>
-        (case e2 of
-         | App (FP_cmp FP_LessEqual) [var2; c2] =>
-         if (var1 ≠ var2) then NONE
-         else
-           (case c1 of
-           | App FpFromWord [Lit (Word64 w1)] =>
-             (case c2 of
-             | App FpFromWord [Lit (Word64 w2)] =>
-               (case var1 of
-               | Var (Short x) =>
-               if (fp64_isFinite w1 ∧ fp64_isFinite w2)
-               then SOME (x, (fp64_to_real w1, fp64_to_real w2))
-               else NONE
-               | _ => NONE)
-             | _ => NONE)
-           | _ => NONE)
-         | _ => NONE)
-      | _ => NONE) ∧
-  getInterval _ = NONE
-End
-
-(**
-  Function toFloVerPre
-  Arguments:
-    CakeML AST of a precondition
-    a 1-1 map from CakeML to FloVer variables
-    The AST of the precondition must be encoded exactly that the top-most
-    conjunct joins either a single constraint (lo ≤ x) ∧ (x ≤ hi), or
-    that it joins a single constraint with the remainder of the precondition
-    ((lo ≤ x) ∧ (x ≤ hi)) ∧ precondition_remainder
-  Returns:
-    A FloVer encoding of the precondition as a function from numbers to
-    reals, and a list of variables bound in the precondition
-    The list is used to make sure that a variable can only be bound once
-    by the precondition in CakeML
-**)
-Definition toFloVerPre_def:
-  toFloVerPre [] ids = NONE ∧
-  toFloVerPre [Log And e1 e2] ids =
-    (* base case: (lo ≤ x ∧ x <= hi) *)
-    (case getInterval (Log And e1 e2) of
-    | SOME (x, lo, hi) =>
-      (case lookupCMLVar (Short x) ids of
-      | NONE => NONE
-      | SOME (y, n) =>
-        SOME ((λ (z:num). if z = n then (lo,hi) else (0:real, 0:real)), [n]))
-    (* compound case: ((lo <= x ∧ x ≤ hi) ∧ remainder *)
-    | NONE =>
-      (* get an interval for the left-hand side of the conjunct *)
-      case getInterval e1 of
-      | NONE => NONE
-      | SOME (x, lo, hi) =>
-      (* get a FloVer variable for the CakeML var from the mapping *)
-      case lookupCMLVar (Short x) ids of
-      | NONE => NONE
-      | SOME (y, n) =>
-      (* recursive translation *)
-      case toFloVerPre [e2] ids of
-      | NONE => NONE
-      | SOME (P, bVars) =>
-      (* check whether the variable is already bound *)
-      case FIND (λ m. n = m) bVars of
-      | SOME _ => NONE  (* cannot rebind variable *)
-      | NONE =>
-        SOME ((λ (z:num). if z = n then (lo,hi) else P z), n :: bVars)) ∧
-  toFloVerPre _ _ = NONE
-End
-
-**)

icing/README.md

@@ -1,58 +1,82 @@
-Icing: CAV'19...
+Main implementation directory for PrincessCake(ML): Verified Compilation and
+Optimization of Floating-Point Programs
+===========================================================================
+
+The development is known to compile with HOL4 commit:
+  52ffdc8f01c5cf044427bf6f3a12e8300e91765a
+
+Running the files in this directory requires a working version of
+[FloVer](https://gitlab.mpi-sws.org/AVA/FloVer).
+You need to download FloVer, compile its HOL4 development and store its
+directory as a shell variable:
+
+```
+git clone  https://gitlab.mpi-sws.org/AVA/FloVer FloVer
+export FLOVERDIR=<current directory>/FloVer/
+cd FloVer/hol4/ && $HOLDIR/bin/Holmake
+```
+
+Afterwards the content in the directory can be build with `Holmake`.
+
+Files contained in this directory:
 
 [CakeMLtoFloVerLemsScript.sml](CakeMLtoFloVerLemsScript.sml):
-Lemmas for connection to FloVer
+Lemmas for connection to FloVer,
+the translation function is defined in CakeMLtoFloVerScript.sml, and the main
+connection theorem in CakeMLtoFloVerProofsScript.sml
 
 [CakeMLtoFloVerProofsScript.sml](CakeMLtoFloVerProofsScript.sml):
-Central theorem about connection to FloVer
+Main connection theorem relating FloVer's roundoff error bound
+to CakeML floating-point kernel executions
 
 [CakeMLtoFloVerScript.sml](CakeMLtoFloVerScript.sml):
-Definition of translation to FloVer
+Translation from CakeML floating-point kernels to FloVer input
 
 [cfSupportScript.sml](cfSupportScript.sml):
-Support lemmas for CF reasoning
+Support lemmas for CF proofs in the end-to-end correctness theorems
 
 [examples](examples):
-Case studies for the Marzipan optimizer
+FPBench benchmarks used in the evaluation of PrincessCake.
 
 [floatToRealProofsScript.sml](floatToRealProofsScript.sml):
-Proofs about translation from float computations to real number computations
+Proofs about translation from floating-point computations to real-number
+computations. Needed to prove simulations in the end-to-end correctness
+theorems.
 
 [floatToRealScript.sml](floatToRealScript.sml):
-Define a translation from float computations to real number computations
+Translation from CakeML floating-point computations to
+CakeML real-number computations.
 
 [icingTacticsLib.sml](icingTacticsLib.sml):
-Tactic library specific to Icing
+Tactic library for PrincessCake development
 
 [icing_optimisationProofsScript.sml](icing_optimisationProofsScript.sml):
-Correctness proofs for Icing optimisations supported by CakeML
-Each optimisation is defined in icing_optimisationsScript.
+Correctness proofs for peephole optimisations supported by PrincessCake
+Each optimisation is defined in icing_optimisationsScript.sml.
 This file proves the low-level correctness theorems for a single
-application of the optimisation, as well as that optimisations
-are real-valued identities.
+application of the optimisation.
+Real-valued identity proofs are in icing_realIdProofsScript.sml.
 The overall correctness proof for a particular run of the optimiser
 from source_to_sourceScript is build using the automation in
 icing_optimisationsLib and the general theorems from
 source_to_sourceProofsScript.
 
 [icing_optimisationsLib.sml](icing_optimisationsLib.sml):
-Library defining function mk_opt_correct_thms that builds an optimiser
-correctness theorem for a list of rewriteFPexp_correct theorems
+Library defining HOL4 automation that builds an optimiser
+correctness theorem for an optimisation plan.
 
 [icing_optimisationsScript.sml](icing_optimisationsScript.sml):
-Icing optimisations supported by CakeML
-This file defines all the optimisations that can be used by the Icing
-optimizer, defined in source_to_sourceScript.
-Correctness proofs for each optimisation are in the file
+Peephole optimisations used by PrincessCake
+This file defines all the optimisations that are can be used by the
+PrincessCake optimiser, defined in source_to_sourceScript.sml .
+The local correctness proofs for each optimisation are in the file
 icing_optimisationProofsScript.
 
 [icing_realIdProofsScript.sml](icing_realIdProofsScript.sml):
 Real-number identity proofs for Icing optimisations supported by CakeML
 Each optimisation is defined in icing_optimisationsScript.
-This file proves the low-level correctness theorems for a single
-application of the optimisation, as well as that optimisations
-are real-valued identities.
-The overall correctness proof for a particular run of the optimiser
+This file proves that optimisations  are real-valued identities.
+The overall real-number simluation proof for a particular run of the optimiser
 from source_to_sourceScript is build using the automation in
 icing_optimisationsLib and the general theorems from
 source_to_sourceProofsScript.
@@ -66,20 +90,30 @@ Implementation of the source to source floating-point rewriter
 This file defines the basic rewriter, used by the optimisation pass later.
 Correctness proofs are in icing_rewriterProofsScript.
 
+[optPlannerProofsScript.sml](optPlannerProofsScript.sml):
+Correctness proof for optimization planner
+
 [optPlannerScript.sml](optPlannerScript.sml):
-Unverified optimisation planners
+Unverified optimisation planner.
+Definitions in this file correspond to the function ‘planOpts’
+from Section 5 of the PrincessCake paper.
 
 [pureExpsScript.sml](pureExpsScript.sml):
 predicate to check whether an expression is pure, i.e. does not use memory
 or the FFI
 
 [source_to_sourceProofsScript.sml](source_to_sourceProofsScript.sml):
-Correctness proofs for floating-point optimizations
+Overall correctness proofs for optimisation functions
+defined in source_to_sourceScript.sml.
+To prove a particular run correct, they are combined
+using the automation in icing_optimisationsLib.sml with
+the local correctness theorems from icing_optimisationProofsScript.sml.
 
 [source_to_sourceScript.sml](source_to_sourceScript.sml):
-Source to source optimiser, applying Icing optimizations
-This file defines the high-level Icing optimisers.
-Their general correctness theorems are proven in source_to_sourceProofsScript.
+This file defines the PrincessCake optimiser as a source to source pass.
+Function ‵stos_pass_with_plans‵ corresponds to ‵applyOpts‵
+from the paper.
+General correctness theorems are proven in source_to_sourceProofsScript.
 The optimiser definitions rely on the low-level functions from
 icing_rewriterScript implementing pattern matching and pattern instantiation.
 

icing/cfSupportScript.sml

@@ -1,5 +1,5 @@
 (**
-  Support lemmas for CF reasoning
+  Support lemmas for CF proofs in the end-to-end correctness theorems
 **)
 open basis_ffiTheory cfHeapsBaseTheory basis;
 open cfTacticsLib ml_translatorLib;

icing/examples/README.md

@@ -1,4 +1,8 @@
-Case studies for the Marzipan optimizer
+FPBench benchmarks used in the evaluation of PrincessCake.
+
+WARNING: Running all of these at once takes a significant amount of time
+as an instance of FloVer will be spawned for all the 44 benchmarks that
+contain no `sqrt` operation.
 
 [RungeKuttaProgCompScript.sml](RungeKuttaProgCompScript.sml):
 Auto-generated by Daisy (https://gitlab.mpi-sws.org/AVA/daisy

icing/examples/RungeKuttaProgCompScript.sml

@@ -161,7 +161,7 @@ Definition theAST_def:
 End
 
 Definition theErrBound_def:
-  theErrBound = inv (2 pow (10))
+  theErrBound = inv (2 pow (5))
 End
 
 val x = define_benchmark theAST_def theAST_pre_def false;

icing/examples/bspline3ProgCompScript.sml

@@ -38,7 +38,7 @@ Definition theAST_def:
 End
 
 Definition theErrBound_def:
-  theErrBound = inv (2 pow (10))
+  theErrBound = inv (2 pow (5))
 End
 
 val x = define_benchmark theAST_def theAST_pre_def true;