Make libmGen compatible with latest changes in HOL4

libmGen/Holmakefile

@@ -2,8 +2,6 @@ INCLUDES = $(HOLDIR)/examples/formal-languages/context-free\
            $(CAKEMLDIR)/developers $(CAKEMLDIR)/misc\
 	   $(CAKEMLDIR)/unverified/sexpr-bootstrap\
 	   $(CAKEMLDIR)/semantics $(CAKEMLDIR)/characteristic\
-	   $(CAKEMLDIR)/compiler $(CAKEMLDIR)/compiler/inference\
-	   $(CAKEMLDIR)/compiler/backend/proofs\
 	   $(CAKEMLDIR)/icing\
 	   $(CAKEMLDIR)/tools/flover\
 	   $(CAKEMLDIR)/tools/dandelion

libmGen/README.md

@@ -0,0 +1,25 @@
+A libm-generator for CakeML that uses Dandelion and FloVer from `tools`
+to prove a specification that relates CakeML code to the real-valued elementary
+function.
+
+[FloVerToCakeMLProofsScript.sml](FloVerToCakeMLProofsScript.sml):
+Main connection theorem relating FloVer's roundoff error bound
+to CakeML floating-point kernel executions
+
+[FloVerToCakeMLScript.sml](FloVerToCakeMLScript.sml):
+Translation from CakeML floating-point kernels to FloVer input
+
+[cosExampleScript.sml](cosExampleScript.sml):
+Example libm function generated from cosine certificate of Dandelion
+
+[expExampleScript.sml](expExampleScript.sml):
+Example libm function generated from cosine certificate of Dandelion
+
+[libmLib.sml](libmLib.sml):
+Implementation of automatic generation of libm functions
+
+[libmScript.sml](libmScript.sml):
+Supporting proofs for automation
+
+[sinExampleScript.sml](sinExampleScript.sml):
+Example libm function generated from sine certificate of Dandelion

libmGen/atnDeg3Script.sml

@@ -0,0 +1,27 @@
+open realZeroLib bitArithLib libmLib preambleDandelion;
+
+val _ = new_theory "atnDeg3";
+
+val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.createMetiTarskiQuery := false;
+
+Definition cos_example_def:
+  cos_example =
+  <|
+  transc := Fun Atn (Var "x");
+  poly := [
+     -6809284315197713  * inv ( 2 pow  84 );
+     8979859070570549  * inv ( 2 pow  53 );
+     2502429001398681  * inv ( 2 pow  78 );
+     -2531269759855903  * inv ( 2 pow  53 );
+    ];
+  eps :=  77569196655847480248172279652945299732867702355  * inv (2 pow 167 );
+  iv := [ ("x",
+    ( -1  * inv (2 pow 1 ),
+      1  * inv (2 pow 1 )))];
+|>
+End
+
+Theorem atn_cml_code_corr = implement cos_example_def "atn"
+
+val _ = export_theory();

libmGen/expDeg4Script.sml

@@ -0,0 +1,29 @@
+open realZeroLib bitArithLib preambleDandelion;
+
+val _ = new_theory "expDeg4";
+
+
+
+Definition exp_example_def:
+  exp_example =
+  <|
+    transc := Fun Exp (Var "x");
+    poly := [
+        2251860978014963  * inv ( 2 pow  51 );
+        2248839599087155  * inv ( 2 pow  51 );
+        1148731941443245  * inv ( 2 pow  51 );
+        2516578118969257  * inv ( 2 pow  54 );
+        5022738147898817  * inv ( 2 pow  56 );
+      ];
+    eps :=  61174722613  * inv (2 pow 51 );
+    iv := [
+        ("x",
+         ( 0 * inv (2 pow 0 ),
+           1 * inv (2 pow 0 )))
+      ];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert exp_example_def “16:num”;
+
+val _ = export_theory();

libmGen/expExampleScript.sml

@@ -0,0 +1,29 @@
+(*
+  Example libm function generated from cosine certificate of Dandelion
+*)
+open libmLib;
+
+val _ = new_theory "expExample";
+
+Definition exp_example_def:
+  exp_example =
+  <|
+    transc := Bop Add (Fun Exp (Bop Mul (Var "x") (Cst (1/2:real)))) (Fun Cos (Bop Mul (Var "x") (Cst (1/2:real))));
+poly := [
+     9007199045267507  * inv ( 2 pow  52 );
+     4503607326537297  * inv ( 2 pow  53 );
+     -3241616109733325  * inv ( 2 pow  69 );
+     375588665660545  * inv ( 2 pow  54 );
+     5979080956143783  * inv ( 2 pow  60 );
+     5038332231908613  * inv ( 2 pow  64 );
+    ];
+  eps :=  27896958177787588423236394485375286824270176601341  * inv (2 pow 192 );
+  iv := [ ("x",
+    ( 37414441915671114706014331717536845303191873100185  * inv (2 pow 168 ),
+      1  * inv (2 pow 0 )))];
+  |>
+End
+
+Theorem cos_cml_code_corr = implement exp_example_def "exp_add_cos"
+
+val _ = export_theory();

libmGen/libmLib.sml

@@ -17,7 +17,7 @@ struct
 
   exception libmGenException of string;
 
-  val approxSteps = “20:num”; (** TODO: make this a parameter ? **)
+  val approxSteps = “16:num”; (** TODO: make this a parameter ? **)
 
   val zero_eq = GSYM $ Q.SPEC ‘1’ REAL_DIV_LZERO
 

libmGen/logAddDeg3Script.sml

@@ -0,0 +1,26 @@
+open realZeroLib bitArithLib libmLib preambleDandelion;
+
+val _ = new_theory "logAddDeg3";
+
+
+
+Definition log_example_def:
+  log_example =
+  <|
+    transc := Fun Log (Bop Add (Var "x") (Cst (1/10))) ;
+  poly := [
+     -1550808607  * inv ( 2 pow  30 );
+     641406787  * inv ( 2 pow  28 );
+     -573949725  * inv ( 2 pow  29 );
+     3766713447  * inv ( 2 pow  34 );
+    ];
+  eps :=  10535917144680386079769337698113777809575837070019  * inv (2 pow 186 );
+  iv := [ ("x",
+    ( 23407410223491741137950216280783988842809415608303  * inv (2 pow 164 ),
+      12861214408511945680192426527903290572972206378189  * inv (2 pow 163 )))];
+|>
+End
+
+Theorem log_cml_code_corr = implement log_example_def "log"
+
+val _ = export_theory();

tools/dandelion/README.md

@@ -0,0 +1,137 @@
+# Dandelion
+
+A certificate checker for approximations of elementary functions.
+
+## Key theorems and definitions relating to the original ITP'22 paper
+
+The first phase is defined across the files `transcApproxSemScript.sml` and
+`approxPolyScript.sml`. The first file defines the overall approximation
+function `approxAsPoly` and gives its soundness proof, and
+`approxPolyScript.sml` defines the low-level approximation function for
+approximating a single elementary function with a single polynomial and proves
+soundness of this function.
+
+Theorem 4 (First Phase Soundness) from section 3 is proven in file
+`transcApproxSemScript.sml` as `approxTransc_sound`.
+Variants of Theorem 5 are proven for the supported elementary function in file
+`mcLaurinApproxScript.sml` if they are not provided by HOL4.
+Variants of Theorem 6 are proven for the supported elementary functions in file
+`approxPolyScript.sml`.
+
+The second phase is implemented and proven sound in the file
+`checkerScript.sml`.
+It relies on the implementation of computable Sturm sequences in
+`sturmComputeScript.sml` and computable polynomial division in
+`euclidDivScript.sml`.
+
+Theorem 7 (Second Phase Soundness) from section 4 is proven in file
+`checkerScript.sml` as the combination of `numZeros_sound`,
+`validBounds_is_valid`, and `validateZerosLeqErr_sound`.
+
+Theorem 8 was ported from Harrison's HOL-Light proofs in file `drangScript.sml`
+and is called `BOUND_THEOREM_INEXACT`.
+
+Theorem 9 (Dandelion soundness) is called `checker_soundness` in file
+`checkerScript.sml`.
+
+The extracted binary is created in the directory `binary`.
+File `translateScript.sml` sets up the CakeML translation of the definitions of
+Dandelion, file `certParserScript.sml` defines our (unverified) parser and
+lexer, file `sturmMainCakeScript.sml` proves the CakeML specification for the
+binary, and file `sturmMainCakeCompileScript.sml` compiles the binary for the
+second phase by running the CakeML compiler in-logic on the translated
+definitions.
+
+[approxCompErrScript.sml](approxCompErrScript.sml):
+Theorems about how to compose errors from truncated Taylor series
+for each supported elementary function
+
+[approxPolyScript.sml](approxPolyScript.sml):
+Function that computes a polynomial approximation for a single elementary
+function on a fixed interval, and its soundness proof.
+Function approxPoly is reused in transcApproxSemScript.sml to build the overall
+function implementing the first phase of Dandelion
+
+[checkerDefsScript.sml](checkerDefsScript.sml):
+Basic definitions used by Dandelion
+
+[checkerScript.sml](checkerScript.sml):
+Define high-level functions used by Dandelion and prove their
+soundness by composing soundness proofs from the included files
+
+[cosDeg3Script.sml](cosDeg3Script.sml):
+Simple cosine of degree 3
+
+[drangScript.sml](drangScript.sml):
+Proofs ported about extrema of real-valued, univariate functions,
+ported from the work by Harrison
+
+[euclidDivScript.sml](euclidDivScript.sml):
+Computable version of polynomial division and a correctness proof.
+Inspired by the implementation in Isabelle/HOL
+isabelle.in.tum.de/library/HOL/HOL-Computational_Algebra/Polynomial.html
+used to implement a computable version of Sturm sequences
+
+[floverConnScript.sml](floverConnScript.sml):
+Connection to FloVer roundoff error analyzer, currently unused
+
+[mcLaurinApproxScript.sml](mcLaurinApproxScript.sml):
+Proofs of McLaurin series for the supported elementary functions
+described in transcLang file
+
+[moreRealScript.sml](moreRealScript.sml):
+small theorems extending HOL4's realTheory
+used throughout the development
+
+[pointCheckerProofsScript.sml](pointCheckerProofsScript.sml):
+Soundness theorem of the point-wise equivalence checker
+Currently unused
+
+[pointCheckerScript.sml](pointCheckerScript.sml):
+A simple checker for polynomial evaluation
+Part one of the soundness proof requires showing that the approximated
+polynomial agrees with what Remez thought the trancendental function behaves
+like on the set of points Ω
+
+[realPolyProofsScript.sml](realPolyProofsScript.sml):
+Some simple properties of polynomials on reals
+
+[realPolyScript.sml](realPolyScript.sml):
+Definition of datatype for real-valued polynomials
+
+[realZeroLib.sml](realZeroLib.sml):
+Library automating Dandelion's certificate validation
+
+[renameScript.sml](renameScript.sml):
+renaming theory to unify naming of theorems
+
+[sinDeg3Script.sml](sinDeg3Script.sml):
+Simple approximation of sine of degree 3
+
+[sturmComputeScript.sml](sturmComputeScript.sml):
+Define a computable version of the sturm sequence and
+prove its equivalence with the non-computable version
+of John Harrison
+
+[sturmScript.sml](sturmScript.sml):
+Proof of Sturm's theorem, ported from Harrison material
+
+[transcApproxSemScript.sml](transcApproxSemScript.sml):
+Define an "approximating" semantics on the elementary functions
+of Dandelion. The function approxTransc corresponds to the
+function "approxAsPoly" in the paper
+
+[transcIntvSemScript.sml](transcIntvSemScript.sml):
+Define an interval semantics on the elementary functions
+of Dandelion. The function borrows the definitions and soundness
+proof of basic arithmetic from FloVer
+
+[transcLangScript.sml](transcLangScript.sml):
+Define a simple "language" for describing elementary
+functions. For now we only allow combinations, i.e.
+exp (sin (cos ...) but no additional operators like +,-,*,/
+
+[transcReflectScript.sml](transcReflectScript.sml):
+Simple reflection function translating elements of the deeply
+embedded transc datatype into the polynomials defined in
+realPolyScript.sml