Modernize FloVer for regression tests

Author: HeikoBecker

icing/flover/CertificateCheckerScript.sml

@@ -13,7 +13,8 @@ open AbbrevsTheory ExpressionsTheory FloverTactics ExpressionAbbrevsTheory
 open preambleFloVer;
 
 val _ = new_theory "CertificateChecker";
-val _ = temp_overload_on("abs",``real$abs``);
+
+Overload abs[local] = “real$abs”;
 
 (** Certificate checking function **)
 Definition CertificateChecker_def:

icing/flover/CertificateGeneratorScript.sml

@@ -1,11 +1,16 @@
+(**
+  A simple, unverified generator for certificates.
+  To be used in conjunction with the certificate checker to first analyze
+  a kernel and then validate the analysis result
+**)
 open RealIntervalInferenceTheory ErrorIntervalInferenceTheory ExpressionsTheory
      FloverMapTheory TypeValidatorTheory CommandsTheory AbbrevsTheory
      ExpressionAbbrevsTheory;
 open preambleFloVer;
 
 val _ = new_theory "CertificateGenerator";
 
-val CertificateGeneratorExp_def = Define `
+Definition CertificateGeneratorExp_def:
   CertificateGeneratorExp (f:real expr) (P:precond) (Gamma:typeMap)
     :(real expr # precond # typeMap # analysisResult) option =
     let
@@ -17,15 +22,18 @@ val CertificateGeneratorExp_def = Define `
         (case inferErrorbound f tMap ivMap FloverMapTree_empty of
         | SOME errMap => SOME (f,P,Gamma,errMap)
         | NONE => NONE)
-      | _, _ => NONE`;
+                    | _, _ => NONE
+End
 
-val getExp_def = Define `
-  getExp (f, P, Gamma, errMap) = f`;
+Definition getExp_def:
+  getExp (f, P, Gamma, errMap) = f
+End
 
-val getError_def = Define `
-  getError (f, P, Gamma, errMap) = FloverMapTree_find f errMap`;
+Definition getError_def:
+  getError (f, P, Gamma, errMap) = FloverMapTree_find f errMap
+End
 
-val CertificateGeneratorCmd_def = Define `
+Definition CertificateGeneratorCmd_def:
   CertificateGeneratorCmd (f:real cmd) (P:precond) (Gamma:typeMap)
     :(real cmd # precond # typeMap # analysisResult) option =
     let
@@ -37,12 +45,15 @@ val CertificateGeneratorCmd_def = Define `
         (case inferErrorboundCmd f tMap ivMap FloverMapTree_empty of
         | SOME errMap => SOME (f,P,Gamma,errMap)
         | NONE => NONE)
-      | _, _ => NONE`;
+                    | _, _ => NONE
+End
 
-val getCmd_def = Define `
-  getCmd (f, P, Gamma, errMap) = f`;
+Definition getCmd_def:
+  getCmd (f, P, Gamma, errMap) = f
+End
 
-val getError_def = Define `
-  getError (f, P, Gamma, errMap) = FloverMapTree_find (getRetExp f) errMap`;
+Definition getError_def:
+  getError (f, P, Gamma, errMap) = FloverMapTree_find (getRetExp f) errMap
+End
 
 val _ = export_theory ();

icing/flover/EnvironmentsScript.sml

@@ -1,11 +1,16 @@
+(**
+  An inductive relation relating real-numbered environments with
+  an environment with "errors", i.e. where variables are bound to
+  finite-precision values
+**)
 open simpLib realTheory realLib RealArith sptreeTheory;
 open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory
      FloverTactics FloverMapTheory MachineTypeTheory;
 open preambleFloVer;
 
 val _ = new_theory "Environments";
 
-val _ = temp_overload_on("abs",``real$abs``);
+Overload abs[local] = “real$abs”
 
 Definition approxEnv_def:
   approxEnv E1 Gamma absEnv (fVars:num_set) (dVars:num_set) E2 =
@@ -98,8 +103,7 @@ Proof
    \\ fs[]
 QED
 
-val approxEnv_rules = LIST_CONJ [approxEnvRefl, approxEnvUpdFree, approxEnvUpdBound]
-val _ = save_thm ("approxEnv_rules", approxEnv_rules);
+Theorem approxEnv_rules = LIST_CONJ [approxEnvRefl, approxEnvUpdFree, approxEnvUpdBound]
 
 Theorem approxEnv_gives_value:
   !E1 E2 x v (fVars:num_set) (dVars:num_set) absenv Gamma.

icing/flover/ErrorBoundsScript.sml

@@ -11,7 +11,8 @@ open preambleFloVer;
 val _ = new_theory "ErrorBounds";
 
 val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
-val _ = temp_overload_on("abs",``real$abs``);
+
+Overload abs[local] = “real$abs”
 
 val triangle_tac =
   irule triangle_trans \\ rpt conj_tac \\ TRY (fs[REAL_ABS_TRIANGLE] \\ NO_TAC);

icing/flover/ErrorIntervalInferenceScript.sml

@@ -1,4 +1,4 @@
- (**
+(**
    This file contains the HOL4 implementation of the error bound validator as well
    as its soundness proof. The function validErrorbound is the Error bound
    validator from the certificate checking process. Under the assumption that a

icing/flover/ErrorValidationScript.sml

@@ -17,11 +17,10 @@ open preambleFloVer;
 val _ = new_theory "ErrorValidation";
 
 val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
-val _ = temp_overload_on("abs",``real$abs``);
-val _ = temp_overload_on("+",``realax$real_add``);
-val _ = temp_overload_on("-",``real$real_sub``);
-val _ = temp_overload_on("*",``realax$real_mul``);
-val _ = temp_overload_on("/",``real$/``);
+
+Overload abs[local] = “real$abs”
+
+val _ = realLib.prefer_real();
 
 val triangle_tac =
   irule triangle_trans \\ fs[REAL_ABS_TRIANGLE];

icing/flover/FPRangeValidatorScript.sml

@@ -18,9 +18,9 @@ open preambleFloVer;
 
 val _ = new_theory "FPRangeValidator";
 
-val _ = temp_overload_on("abs",``real$abs``);
+Overload abs[local] = “real$abs”
 
-val FPRangeValidator_def = Define `
+Definition FPRangeValidator_def:
   FPRangeValidator (e:real expr) A typeMap dVars =
     case FloverMapTree_find e A, FloverMapTree_find e typeMap of
       | SOME (iv_e, err_e), SOME m =>
@@ -58,28 +58,31 @@ val FPRangeValidator_def = Define `
                       then normal_or_zero /\ recRes
                       else
                           F)
-      | _, _ => F`;
+      | _, _ => F
+End
 
-val normalOrZero_def = Define `
+Definition normalOrZero_def:
   normalOrZero iv_e_float m =
     ((normal (IVlo iv_e_float) m \/ (IVlo iv_e_float) = 0) /\
-     (normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0))`;
+     (normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0))
+End
 
-val FPRangeValidatorCmd_def = Define `
+Definition FPRangeValidatorCmd_def:
   (FPRangeValidatorCmd ((Let m x e g):real cmd) A typeMap dVars =
      if FPRangeValidator e A typeMap dVars
      then FPRangeValidatorCmd g A typeMap (insert x () dVars)
      else F) /\
   (FPRangeValidatorCmd (Ret e) A typeMap dVars =
-   FPRangeValidator e A typeMap dVars)`;
+   FPRangeValidator e A typeMap dVars)
+End
 
-val enclosure_to_abs = store_thm (
-  "enclosure_to_abs",
-  ``!a b c.
+Theorem enclosure_to_abs:
+  !a b c.
      a <= b /\ b <= c /\
     (0 < a \/ c < 0 ) ==>
     (abs a <= abs b /\ abs b <= abs c) \/
-    (abs c <= abs b /\ abs b <= abs a)``,
+    (abs c <= abs b /\ abs b <= abs a)
+Proof
   rpt strip_tac \\ fs[]
   >- (`0 < b` by REAL_ASM_ARITH_TAC
       \\ `0 <= a /\ 0 <= b` by REAL_ASM_ARITH_TAC
@@ -91,21 +94,22 @@ val enclosure_to_abs = store_thm (
   >- (`~ (0 <= b)` by REAL_ASM_ARITH_TAC
       \\ `~ (0 <= a)` by REAL_ASM_ARITH_TAC
       \\ `~ (0 <= c)` by REAL_ASM_ARITH_TAC
-      \\ fs[realTheory.abs]));
+      \\ fs[realTheory.abs])
+QED
 
 fun assume_all l =
   case l of
       t :: ls => assume_tac t \\ assume_all ls
     | NIL =>  ALL_TAC;
 
-val normal_enclosing = store_thm (
-  "normal_enclosing",
-  ``!v m vHi vLo.
+Theorem normal_enclosing:
+  !v m vHi vLo.
       (0 < vLo \/ vHi < 0) /\
       normal vLo m /\
       normal vHi m /\
       vLo <= v /\ v <= vHi ==>
-    normal v m``,
+      normal v m
+Proof
   rpt gen_tac
   \\ disch_then (fn thm => assume_all (CONJ_LIST 4  thm))
   \\ `(abs vLo <= abs v /\ abs v <= abs vHi) \/ (abs vHi <= abs v /\ abs v <= abs vLo)`
@@ -114,7 +118,8 @@ val normal_enclosing = store_thm (
   \\ fs[normal_def]
   \\ rveq
   \\ fs[]
-  \\ RealArith.REAL_ASM_ARITH_TAC);
+  \\ RealArith.REAL_ASM_ARITH_TAC
+QED
 
 val solve_tac =
   rpt (qpat_x_assum `!x. _` kall_tac)

icing/flover/IEEE_connectionScript.sml

@@ -1,3 +1,7 @@
+(**
+  Connect FloVer's idealized machine semantics to 64-bit
+  IEEE-754 floating-point semantics
+**)
 open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory RealArith;
 open MachineTypeTheory ExpressionsTheory RealSimpsTheory FloverTactics
      CertificateCheckerTheory FPRangeValidatorTheory IntervalValidationTheory
@@ -9,7 +13,8 @@ open preambleFloVer;
 
 val _ = new_theory "IEEE_connection";
 
-val _ = temp_overload_on("abs",``real$abs``);
+Overload abs[local] = “real$abs”
+
 val _ = diminish_srw_ss ["RMULCANON_ss","RMULRELNORM_ss"]
 
 (** FloVer assumes rounding with ties to even, thus we exprlicitly define
@@ -295,30 +300,41 @@ Proof
   \\ `w2n c0 = 2047` by fs[] \\ fs[]
   \\ TOP_CASE_TAC \\ fs[minValue_pos_def, minExponentPos_def]
   \\ fs[REAL_ABS_MUL, POW_M1]
-  >- (`44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304⁻¹ <=  inv 1`
-        by (irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
-      \\ fs[pow_simp1, REAL_DIV_LZERO, ABS_1, REAL_OF_NUM_POW, abs]
-      \\ `179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216 < inv 1`
-      by (irule REAL_LTE_TRANS \\ asm_exists_tac \\ fs[])
-      \\ fs[REAL_INV1])
+  >- (
+    qpat_x_assum ‘_ < inv _’ mp_tac
+    \\ qmatch_goalsub_abbrev_tac ‘_ < inv cst1 ⇒ _’
+    \\ strip_tac
+    \\ `inv cst1 <= inv 1`
+        by (unabbrev_all_tac \\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
+    \\ fs[pow_simp1, REAL_DIV_LZERO, ABS_1, REAL_OF_NUM_POW, abs]
+    \\ qpat_x_assum ‘_ < inv cst1’ mp_tac
+    \\ qmatch_goalsub_abbrev_tac ‘cst2 < inv cst1’ \\ strip_tac
+    \\ `cst2 < inv 1`
+      by (unabbrev_all_tac \\ irule REAL_LTE_TRANS \\ asm_exists_tac \\ fs[])
+    \\ unabbrev_all_tac \\ fs[REAL_INV1])
   \\ Cases_on `c1` \\ fs[]
   \\ `1 < abs (1 + &n / 4503599627370496)`
-    by (
-    fs[abs]
-    \\ `0:real <= 1 + &n / 4503599627370496`
-           by (irule REAL_LE_TRANS
-               \\ qexists_tac `1` \\ fs[]
-               \\ irule REAL_LE_DIV \\ fs[])
-    \\ fs[]
-    \\ once_rewrite_tac [GSYM REAL_ADD_RID]
-    \\ once_rewrite_tac [GSYM REAL_ADD_ASSOC]
-    \\ fs[]
-    \\ irule REAL_LT_DIV \\ fs[])
-  \\ `44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304⁻¹ <=  inv 1`
-    by (irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
+    by (fs[abs]
+        \\ `0:real <= 1 + &n / 4503599627370496`
+               by (irule REAL_LE_TRANS
+                   \\ qexists_tac `1` \\ fs[]
+                   \\ irule REAL_LE_DIV \\ fs[])
+        \\ fs[]
+        \\ once_rewrite_tac [GSYM REAL_ADD_RID]
+        \\ once_rewrite_tac [GSYM REAL_ADD_ASSOC]
+        \\ fs[]
+        \\ irule REAL_LT_DIV \\ fs[])
+  \\ qpat_x_assum ‘_ < inv _’ mp_tac
+  \\ qmatch_goalsub_abbrev_tac ‘_ < inv cst1 ⇒ _’
+  \\ `inv cst1 <=  inv 1`
+    by (unabbrev_all_tac \\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
+  \\ strip_tac
   \\ fs[pow_simp1, REAL_DIV_LZERO, ABS_1, REAL_OF_NUM_POW, abs]
-  \\ `179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216 < inv 1`
-    by (irule REAL_LTE_TRANS \\ once_rewrite_tac[CONJ_COMM]
+  \\ qpat_x_assum ‘_ < inv cst1’ mp_tac
+  \\ qmatch_goalsub_abbrev_tac ‘(cst2 * _) < inv cst1’
+  \\ strip_tac
+  \\ `cst2 < inv 1`
+    by (unabbrev_all_tac \\ irule REAL_LTE_TRANS \\ once_rewrite_tac[CONJ_COMM]
         \\ rewrite_tac[REAL_INV1] \\ asm_exists_tac \\ fs[]
         \\ qmatch_goalsub_abbrev_tac `cst1 < cst2`
         \\ `0 <= (1:real) + &n / 4503599627370496`
@@ -332,7 +348,7 @@ Proof
         \\ once_rewrite_tac [GSYM REAL_MUL_ASSOC] \\ irule REAL_LT_LMUL_IMP
         \\ fs[]
         \\ unabbrev_all_tac \\ fs[])
-  \\ fs[REAL_INV1]
+  \\ unabbrev_all_tac \\ fs[REAL_INV1]
 QED
 
 Theorem validValue_gives_float_value:

icing/flover/Infra/FloverCompLib.sml

@@ -1,3 +1,6 @@
+(**
+  Small changes to computeLib for FloVer
+**)
 structure FloverCompLib =
 struct
 open computeLib;

icing/flover/Infra/Holmakefile

@@ -1,3 +1,8 @@
-INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple $(HOLDIR)/examples/fun-op-sem/lprefix_lub
-
 OPTIONS = QUIT_ON_FAILURE
+
+all: $(DEFAULT_TARGETS) README.md
+
+README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
+DIRS = $(wildcard */)
+README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
+	$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)

icing/flover/Infra/MachineTypeScript.sml

@@ -10,11 +10,11 @@ open preambleFloVer;
 
 val _ = new_theory "MachineType";
 
-val _ = temp_overload_on("abs",``real$abs``);
+Overload abs[local] = “real$abs”
+
 val _ = monadsyntax.enable_monadsyntax();
 val _ = List.app monadsyntax.enable_monad ["option"];
 
-
 Datatype:
   mType = REAL | M16 | M32 | M64 | F num num bool (* first num is word length, second is fractional bits, bool is for sign of fractional bits *)
 End