Merge branch 'reworked-ci' into 'master'

Rework CI to properly deal with HOL4

See merge request AVA/FloVer!4

.gitlab-ci.yml

-image: localhost:5000/flover
+image: heikobecker/coq-polyml-ci
 
 variables:
     GIT_SUBMODULE_STRATEGY: none
 
 stages:
   - compile
-  - regression
+#  - regression
 
 compile-coq:
   stage: compile
@@ -23,6 +23,6 @@ compile-hol:
     paths:
     - hol4/binary/
 
-regression-tests:
-  stage: regression
-  script: ./scripts/regressiontests.sh
\ No newline at end of file
+# regression-tests:
+#  stage: regression
+#  script: ./scripts/regressiontests.sh
\ No newline at end of file

Dockerfile

@@ -15,31 +15,18 @@ RUN opam init --comp=4.05.0 --auto-setup && \
 
 # Install coq and dependencies
 RUN opam repo add coq-released https://coq.inria.fr/opam/released && \
-    opam update && \
-    opam install coq.8.7.2 coq-flocq
+    opam update
+
+#Install coq 8.7.2 in a switch
+RUN opam switch -A 4.05.0 coq8.7.2
+RUN opam install coq.8.7.2 coq-flocq.2.6.1
+
+#Install coq 8.8 in a switch
+RUN opam switch -A 4.05.0 coq8.8
+RUN opam install coq.8.8.0 coq-flocq.2.6.1
 
 # Install polyml from git
 RUN git clone https://github.com/polyml/polyml.git polyml && \
     cd polyml && \
     git checkout v5.7 && \
     ./configure && make && make install
-
-ADD ./hol4/.HOLCOMMIT /root/HOLCOMMIT
-
-# RUN cat /root/HOLCOMMIT
-
-# RUN export HOLCOMMIT="$(cat /root/HOLCOMMIT)"
-
-# RUN echo $HOLCOMMIT
-
-# Download HOL4 and compile
-RUN git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4 && \
-    cd HOL4 && \
-    git checkout `cat /root/HOLCOMMIT` &&\
-    git rev-parse HEAD &&\
-    poly < tools/smart-configure.sml && \
-    ./bin/build
-
-RUN echo "HOLDIR=/root/HOL4" >> /root/.profile
-
-ENV HOLDIR /root/HOL4

coq/configure_coq.sh

@@ -25,7 +25,9 @@ fi
 coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
 case "$coq_ver" in
     8.7.2)
-       ;;
+    ;;
+    8.8.0)
+    ;;
     *)
         echo "Error: Need 8.7.2"
         exit 1

coq/floverParser.v

@@ -12,8 +12,9 @@ Inductive Token:Type :=
 | DCOND
 | DGAMMA
 | DTYPE:mType -> Token
+| DFIXED
 | DVAR
-| DCONST: N -> Token
+| DCONST: nat -> Token
 | DNEG
 | DPLUS
 | DSUB
@@ -32,7 +33,7 @@ Definition getChar (input:string):=
   end.
 
 Definition getConst (c:ascii) :=
-  ((N_of_ascii c) - 48)%N.
+  ((nat_of_ascii c) - 48)%nat.
 
 Definition suffix (s:string) :=
 match s with
@@ -50,7 +51,7 @@ Definition isAlpha (c:ascii) :bool :=
 Definition isAlphaNum (c :ascii) :bool :=
   isDigit c || isAlpha c.
 
-Fixpoint lexConst (input:string) (akk:N) :=
+Fixpoint lexConst (input:string) (akk:nat) :=
   match input with
   |String c input' =>
    if (isDigit c)
@@ -97,10 +98,14 @@ match fuel with
                  | "GAMMA" => DGAMMA :: lex input'' fuel'
                  | "Var" => DVAR :: lex input'' fuel'
                  | "Cast" => DCAST :: lex input'' fuel'
+                 | "F" => DFIXED :: lex input'' fuel'
                  | "MTYPE" => let ts := lex input'' fuel' in
                               (match ts with
+                               |DCONST 16 :: ts' => DTYPE M16 :: ts'
                                |DCONST 32 :: ts' => DTYPE M32 :: ts'
                                |DCONST 64 :: ts' => DTYPE M64 :: ts'
+                               |DFIXED :: DCONST w :: DCONST f :: ts' =>
+                                DTYPE (F (Pos.of_nat w) (Pos.of_nat f)) :: ts'
                             (* | DCONST 128 :: ts' => DTYPE M128 :: ts' *)
                             (* | DCONST 256 :: ts' => DTYPE M256 :: ts' *)
                                | _ => []
@@ -154,9 +159,10 @@ Definition pp_token (token:Token) :=
   | DABS => "ABS"
   | DCOND => "?"
   | DVAR => "Var"
-  | DCONST num => str_of_num (N.to_nat num) (N.to_nat num)
+  | DCONST num => str_of_num num num
   | DGAMMA => "Gamma"
   | DTYPE m => str_join "MTYPE " (type_to_string m)
+  | DFIXED => ""
   | DNEG => "~"
   | DPLUS => "+"
   | DSUB => "-"
@@ -181,10 +187,10 @@ Fixpoint parseExp (tokList:list Token) (fuel:nat):option (expr Q * list Token) :
      match tokList with
      | DCONST n :: DFRAC :: DCONST m :: DTYPE t :: tokRest =>
        match m with
-       |N0 => None
-       |Npos p => Some (Const t (Z.of_N n # p), tokRest)
+       | 0%nat => None
+       |S p => Some (Const t (Z.of_nat n # (Pos.of_nat p)), tokRest)
        end
-     | DVAR :: DCONST n :: tokRest => Some (Var Q (N.to_nat n), tokRest)
+     | DVAR :: DCONST n :: tokRest => Some (Var Q n, tokRest)
      | DNEG :: tokRest =>
        match (parseExp tokRest fuel') with
        | Some (Const m c, tokRest) => Some (Const m (- c), tokRest)
@@ -259,7 +265,7 @@ Fixpoint parseLet input fuel:option (cmd Q * list Token) :=
                (* Parse it *)
                match (parseLet letBodyRest fuel') with
                (* And construct a result from it *)
-               | Some (letCmd, arbRest) => Some (Let m (N.to_nat n) e letCmd, arbRest)
+               | Some (letCmd, arbRest) => Some (Let m n e letCmd, arbRest)
                | _ => None
                end
              (* But if we have a return *)
@@ -267,7 +273,7 @@ Fixpoint parseLet input fuel:option (cmd Q * list Token) :=
                (* parse only this *)
                match (parseRet retBodyRest fuel) with
                (* and construct the result *)
-               | Some (retCmd, arbRest) => Some (Let m (N.to_nat n) e retCmd, arbRest)
+               | Some (retCmd, arbRest) => Some (Let m n e retCmd, arbRest)
                | _ => None
                end
              | _ => None (* fail if there is no continuation for the let *)
@@ -283,13 +289,13 @@ Definition parseFrac (input:list Token) :option (Q * list Token) :=
   match input with
   | DNEG :: DCONST n :: DFRAC :: DCONST m :: tokRest =>
     match m with
-    |N0 => None
-    |Npos p => Some ((- Z.of_N n # p),tokRest)
+    |0%nat => None
+    |S p => Some ((- Z.of_nat n # Pos.of_nat p),tokRest)
     end
   | DCONST n :: DFRAC :: DCONST m :: tokRest =>
     match m with
-    |N0 => None
-    |Npos p => Some ((Z.of_N n # p),tokRest)
+    |0%nat => None
+    |S p => Some ((Z.of_nat n # Pos.of_nat p),tokRest)
     end
   | _ => None
   end.
@@ -322,8 +328,8 @@ Fixpoint parsePrecondRec (input:list Token) (fuel:nat) :option (precond * list T
        match parseIV fracRest with
        | Some (iv, precondRest) =>
          match parsePrecondRec precondRest fuel' with
-         | Some (P, tokRest) => Some (updPre (N.to_nat n) iv P, tokRest)
-         | None => Some (updPre (N.to_nat n) iv defaultPre, precondRest)
+         | Some (P, tokRest) => Some (updPre n iv P, tokRest)
+         | None => Some (updPre n iv defaultPre, precondRest)
          end
        | _ => None
        end
@@ -386,7 +392,7 @@ Fixpoint parseGammaRec (input: list Token) : option ((nat -> option mType) * lis
   match input with
   | DVAR :: DCONST n :: DTYPE m :: inputRest =>
     match parseGammaRec inputRest with
-    | Some (Gamma, rest) => Some (updDefVars (N.to_nat n) m Gamma, rest)
+    | Some (Gamma, rest) => Some (updDefVars n m Gamma, rest)
     | None => None
      end
   | _  => Some (defaultGamma, input)
@@ -542,6 +548,6 @@ Fixpoint check_all (num_fun:nat) (iters:nat) (input:list Token) fuel:=
 Definition runChecker (input:string) :=
   let tokList := lex input (str_length input) in
   match tokList with
-  | DCONST n :: DCONST m :: tokRest => check_all (N.to_nat m) (N.to_nat n)  tokRest (List.length tokList * 100)
+  | DCONST n :: DCONST m :: tokRest => check_all m n tokRest (List.length tokList * 100)
   | _ => "failure no num of functions"
   end.

hol4/CertificateCheckerScript.sml

@@ -44,7 +44,7 @@ val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
       CertificateChecker e A P defVars ==>
       ?iv err vR vF m.
         FloverMapTree_find e A = SOME (iv,err) /\
-        eval_exp E1 (toRMap defVars) (toREval e) vR M0 /\
+        eval_exp E1 (toRMap defVars) (toREval e) vR REAL /\
         eval_exp E2 defVars e vF m /\
         (!vF m.
            eval_exp E2 defVars e vF m ==>
@@ -99,7 +99,7 @@ val CertificateCmd_checking_is_sound = store_thm ("CertificateCmd_checking_is_so
       CertificateCheckerCmd f A P defVars ==>
       ?iv err vR vF m.
         FloverMapTree_find (getRetExp f) A = SOME (iv, err) /\
-        bstep (toREvalCmd f) E1 (toRMap defVars) vR M0 /\
+        bstep (toREvalCmd f) E1 (toRMap defVars) vR REAL /\
         bstep f E2 defVars vF m /\
         (!vF m. bstep f E2 defVars vF m ==> abs (vR - vF) <= err)``,
   simp [CertificateCheckerCmd_def]

hol4/CommandsScript.sml

@@ -20,7 +20,7 @@ val _ = Datatype `
 val toREvalCmd_def = Define `
   toREvalCmd (f:real cmd) : real cmd =
 	case f of
-	  | Let m x e g => Let M0 x (toREval e) (toREvalCmd g)
+	  | Let m x e g => Let REAL x (toREval e) (toREvalCmd g)
 	  | Ret e => Ret (toREval e)`;
 
 (**

hol4/EnvironmentsScript.sml

@@ -12,7 +12,7 @@ val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
   (!(E1:env) (E2:env) (defVars: num -> mType option) (A:analysisResult) (fVars:num_set) (dVars:num_set) v1 v2 x.
       approxEnv E1 defVars A fVars dVars E2 /\
       (defVars x = SOME m) /\
-      (abs (v1 - v2) <= abs v1 * (mTypeToQ m)) /\
+      (abs (v1 - v2) <= computeError v1  m) /\
       (lookup x (union fVars dVars) = NONE) ==>
       approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A (insert x () fVars) dVars (updEnv x v2 E2)) /\
   (!(E1:env) (E2:env) (defVars: num -> mType option) (A:analysisResult)
@@ -58,7 +58,7 @@ val approxEnv_fVar_bounded = store_thm (
       E2 x = SOME v2 /\
       x IN (domain fVars) /\
       Gamma x = SOME m ==>
-      abs (v - v2) <= (abs v) * (mTypeToQ m)``,
+      abs (v - v2) <= computeError v m``,
   rpt strip_tac
   \\ qspec_then
       `\E1 Gamma absenv fVars dVars E2.
@@ -67,7 +67,7 @@ val approxEnv_fVar_bounded = store_thm (
          E2 x = SOME v2 /\
          x IN (domain fVars) /\
          Gamma x = SOME m ==>
-         abs (v - v2) <= (abs v) * (mTypeToQ m)`
+         abs (v - v2) <= computeError v m`
       (fn thm => irule (SIMP_RULE std_ss [] thm))
       approxEnv_ind
   \\ rpt strip_tac

hol4/FPRangeValidatorScript.sml

@@ -150,7 +150,7 @@ val FPRangeValidator_sound = store_thm (
           \\ disch_then drule \\ fs[])
   \\ once_rewrite_tac [validFloatValue_def]
   \\ `?iv err vR. FloverMapTree_find e A = SOME (iv, err) /\
-        eval_exp E1 (toRMap Gamma) (toREval e) vR M0 /\
+        eval_exp E1 (toRMap Gamma) (toREval e) vR REAL /\
         FST iv <= vR /\ vR <= SND iv`
        by (drule validIntervalbounds_sound
            \\ disch_then (qspecl_then [`fVars`, `E1`, `Gamma`] impl_subgoal_tac)
@@ -256,7 +256,7 @@ val FPRangeValidatorCmd_sound = store_thm (
                \\ rpt strip_tac
                \\ metis_tac[])
            >- (irule swap_Gamma_bstep
-               \\ qexists_tac `updDefVars n M0 (toRMap Gamma)` \\ fs[]
+               \\ qexists_tac `updDefVars n REAL (toRMap Gamma)` \\ fs[]
                \\ fs [updDefVars_def, REWRITE_RULE [updDefVars_def] Rmap_updVars_comm])
            >- (fs[DIFF_DEF, domain_insert, SUBSET_DEF]
                \\ rpt strip_tac \\ first_x_assum irule

hol4/Infra/FloverTactics.sml

@@ -196,6 +196,27 @@ fun Flover_compute t =
               (split_pair_case_tac)) \\ fs[])))
     end;
 
+fun iter_exists_tac ind n =
+  fn tm =>
+    if ind < n
+    then
+      (part_match_exists_tac
+        (fn concl => List.nth (strip_conj concl, ind)) tm)
+        ORELSE (iter_exists_tac (ind+1) n tm)
+    else
+      FAIL_TAC (concat ["No matching clause found for ", term_to_string tm]) ;
+
+val try_all:term -> tactic =
+  fn tm =>
+    fn (asl, g) =>
+      let
+        val len = length (strip_conj (snd (dest_exists g))) in
+        iter_exists_tac 0 len tm (asl, g)
+     end;
+
+val find_exists_tac =
+  first_assum (try_all o concl);
+
 (* val Flover_compute:tactic = *)
 (*     fn (g:goal) => *)
 (*        let *)
@@ -206,4 +227,5 @@ fun Flover_compute t =
 (*                Flover_compute_steps terms_to_eval g *)
 (*   end; *)
 
+
 end

hol4/Infra/MachineTypeScript.sml

@@ -4,59 +4,92 @@
   @author: Raphael Monat
   @maintainer: Heiko Becker
  **)
-open miscTheory realTheory realLib sptreeTheory
-open preamble
+open realTheory realLib sptreeTheory;
+open RealSimpsTheory;
+open preamble;
 
 val _ = new_theory "MachineType";
 
 val _ = temp_overload_on("abs",``real$abs``);
 
 val _ = Datatype `
-  mType = M0 | M16 |  M32 | M64(* | M128 | M256 *)`;
+  mType = REAL | M16 |  M32 | M64(* | M128 | M256 *)
+          |F num num (*first num is word length, second is fractional bits *)`;
 
-val mTypeToQ_def = Define `
-  mTypeToQ (m:mType) : real =
+val mTypeToR_def = Define `
+  mTypeToR (m:mType) : real =
     case m of
-      | M0 => 0
+      | REAL => 0
       | M16 => 1 / (2 pow 11)
       | M32 => 1 / (2 pow 24)
       | M64 => 1 / (2 pow 53)
+      | F w f => 1 / (2 pow f)
       (* the epsilons below match what is used internally in flover,
          although these value do not match the IEEE standard *)
       (* | M128 => 1 / (2 pow 105) *)
       (* | M256 => 1 / (2 pow 211) *)`;
 
-val meps_def = Define `meps = mTypeToQ`;
-
-val mTypeToQ_pos = store_thm("mTypeToQ_pos",
-  ``!e. 0 <= mTypeToQ e``,
-  Cases_on `e` \\ EVAL_TAC);
+val computeError_def = Define `
+  computeError v m =
+    case m of
+    | REAL => 0
+    | F w f => mTypeToR m
+    | _ => abs v * mTypeToR m`;
+
+val mTypeToR_pos = store_thm("mTypeToR_pos",
+  ``!e. 0 <= mTypeToR e``,
+  Cases_on `e` \\ TRY EVAL_TAC
+  \\ fs[]);
+
+val computeError_up = store_thm (
+  "computeError_up",
+  ``!v a b m.
+      abs v <= maxAbs (a,b) ==>
+      computeError v m <= computeError (maxAbs (a,b)) m``,
+  rpt strip_tac \\ Cases_on `m` \\ fs[mTypeToR_def, computeError_def] \\ TRY RealArith.REAL_ASM_ARITH_TAC
+  \\ irule REAL_LE_RMUL_IMP \\ fs[]
+  \\ fs[maxAbs_def]
+  \\ `abs (real$max (abs a) (abs b)) = real$max (abs a) (abs b)`
+        by (once_rewrite_tac[ABS_REFL]
+            \\ fs[max_def]
+            \\ Cases_on `abs a <= abs b`\\ fs[]
+            \\ irule REAL_ABS_POS)
+  \\ fs[]);
 
 (**
   Check if machine precision m1 is more precise than machine precision m2.
-  M0 is real-valued evaluation, hence the most precise.
+  REAL is real-valued evaluation, hence the most precise.
   All others are compared by
-    mTypeToQ m1 <= mTypeToQ m2
+    mTypeToR m1 <= mTypeToR m2
  **)
 val isMorePrecise_def = Define `
-  isMorePrecise (m1:mType) (m2:mType) = (mTypeToQ (m1) <= mTypeToQ (m2))`;
+  isMorePrecise (m1:mType) (m2:mType) =
+    case m1, m2 of
+    | REAL, _ => T
+    | F w1 f1, F w2 f2 => w1 <= w2
+    | F w f, _ => F
+    | _, F w f => F
+    | _, _ => (mTypeToR (m1) <= mTypeToR (m2))`;
 
 val morePrecise_def = Define `
-  (morePrecise M0 _ = T) /\
+  (morePrecise REAL _ = T) /\
+  (morePrecise (F w1 f1) (F w2 f2) = (w1 <= w2)) /\
+  (morePrecise (F w f) _ = F) /\
+  (morePrecise _ (F w f) = F) /\
   (morePrecise M16 M16 = T) /\
   (morePrecise M32 M32 = T) /\
   (morePrecise M32 M16 = T) /\
-  (morePrecise M64 M0 = F) /\
+  (morePrecise M64 REAL = F) /\
   (morePrecise M64 _ = T) /\
   (morePrecise _ _ = F) `;
 
-val morePrecise_antisym = store_thm (
-  "morePrecise_antisym",
-  ``!m1 m2.
-      morePrecise m1 m2 /\
-      morePrecise m2 m1 ==>
-      m1 = m2``,
- rpt strip_tac \\ Cases_on `m1` \\ Cases_on `m2` \\ fs[morePrecise_def]);
+(* val morePrecise_antisym = store_thm ( *)
+(*   "morePrecise_antisym", *)
+(*   ``!m1 m2. *)
+(*       morePrecise m1 m2 /\ *)
+(*       morePrecise m2 m1 ==> *)
+(*       m1 = m2``, *)
+(*  rpt strip_tac \\ Cases_on `m1` \\ Cases_on `m2` \\ fs[morePrecise_def]); *)
 
 val morePrecise_trans = store_thm (
   "morePrecise_trans",
@@ -74,20 +107,21 @@ val isMorePrecise_morePrecise = store_thm (
     isMorePrecise m1 m2 = morePrecise m1 m2``,
   rpt strip_tac
   \\ Cases_on `m1` \\ Cases_on `m2`
-  \\ fs[morePrecise_def, isMorePrecise_def, mTypeToQ_def]);
+  \\ once_rewrite_tac [morePrecise_def, isMorePrecise_def]
+  \\ fs[morePrecise_def, isMorePrecise_def, mTypeToR_def]);
 
-val M0_least_precision = store_thm ("M0_least_precision",
+val REAL_least_precision = store_thm ("REAL_least_precision",
   ``!(m:mType).
-      isMorePrecise m M0 ==>
-      m = M0``,
-  fs [isMorePrecise_def, mTypeToQ_def] \\
+      isMorePrecise m REAL ==>
+      m = REAL``,
+  fs [isMorePrecise_def, mTypeToR_def] \\
   rpt strip_tac \\
   Cases_on `m` \\
   fs []);
 
-val M0_lower_bound  = store_thm ("M0_lower_bound",
+val REAL_lower_bound  = store_thm ("REAL_lower_bound",
   ``! (m:mType).
-      isMorePrecise M0 m``,
+      isMorePrecise REAL m``,
   Cases_on `m` \\ EVAL_TAC);
 
 (**
@@ -102,35 +136,37 @@ val join_def = Define `
 val join3_def = Define `
   join3 (m1: mType) (m2: mType) (m3: mType) = join m1 (join m2 m3)`;
 
-(* val M0_join_is_M0 = store_thm ("M0_join_is_M0", *)
+(* val REAL_join_is_REAL = store_thm ("REAL_join_is_REAL", *)
 (*   ``!m1 m2. *)
-(*       join m1 m2 = M0 ==> *)
-(*       (m1 = M0 /\ m2 = M0)``, *)
+(*       join m1 m2 = REAL ==> *)
+(*       (m1 = REAL /\ m2 = REAL)``, *)
 (*   fs [join_def, isMorePrecise_def] *)
 (*   \\ rpt strip_tac *)
-(*   \\ Cases_on `m1 = M0` \\ Cases_on `m2 = M0` \\ fs[] *)
-(*   >- (m1 = M0 by (Cases_on `mTypeToQ m1 <= mTypeToQ M0` \\ fs[] *)
-(*   \\ fs [ONCE_REWRITE_RULE [isMorePrecise_def] M0_least_precision] *)
-(*   \\ Cases_on `m1` \\ fs[mTypeToQ_def] *)
-(*   \\ Cases_on `m2` \\ fs[mTypeToQ_def] *)
-(*   qpat_x_assum `_ = M0` *)
+(*   \\ Cases_on `m1 = REAL` \\ Cases_on `m2 = REAL` \\ fs[] *)
+(*   >- (m1 = REAL by (Cases_on `mTypeToR m1 <= mTypeToR REAL` \\ fs[] *)
+(*   \\ fs [ONCE_REWRITE_RULE [isMorePrecise_def] REAL_least_precision] *)
+(*   \\ Cases_on `m1` \\ fs[mTypeToR_def] *)
+(*   \\ Cases_on `m2` \\ fs[mTypeToR_def] *)
+(*   qpat_x_assum `_ = REAL` *)
 (*     (fn thm => fs [thm]) *)
-(*   >- (Cases_on `m1` \\ fs [mTypeToQ_def]) *)
-(*   >- (Cases_on `m2` \\ fs [mTypeToQ_def])); *)
+(*   >- (Cases_on `m1` \\ fs [mTypeToR_def]) *)
+(*   >- (Cases_on `m2` \\ fs [mTypeToR_def])); *)
 
 val maxExponent_def = Define `
-  (maxExponent (M0) = 0n) /\
+  (maxExponent (REAL) = 0n) /\
   (maxExponent (M16) = 15) /\
   (maxExponent (M32) = 127) /\
-  (maxExponent (M64) = 1023)
+  (maxExponent (M64) = 1023) /\
+  (maxExponent (F w f) = f)
      (* | M128 => 1023 (** FIXME **) *)
      (* | M256 => 1023 *)`;
 
 val minExponentPos_def = Define `
-  (minExponentPos (M0) = 0n) /\
+  (minExponentPos (REAL) = 0n) /\
   (minExponentPos (M16) = 14) /\
   (minExponentPos (M32) = 126) /\
-  (minExponentPos (M64) = 1022) (*/\ *)
+  (minExponentPos (M64) = 1022) /\
+  (minExponentPos (F w f) = f) (*/\ *)
   (* (minExponentPos (M128) = 1022) /\ (* FIXME *) *)
   (* (minExponentPos (M256) = 1022) *)`;
 
@@ -142,12 +178,18 @@ which simplifies to 2^(e_max) for base 2
 **)
 
 val maxValue_def = Define `
-  maxValue (m:mType) = (&(2n ** (maxExponent m))):real`;
+  maxValue (m:mType) =
+    case m of
+    | F w f => &((2n ** (w-1)) - 1) * &(2n ** (maxExponent m))
+    | _ => (&(2n ** (maxExponent m))):real`;
 
 (** Using the sign bit, the very same number is representable as a negative number,
   thus just apply negation here **)
-val minValue_def = Define `
- minValue (m:mType) = inv (&(2n ** (minExponentPos m)))`;
+val minValue_pos_def = Define `
+  minValue_pos (m:mType) =
+    case m of
+    | F w f => 0
+    | _ =>  inv (&(2n ** (minExponentPos m)))`;
 
 
 (** Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
@@ -159,13 +201,13 @@ val minDenormalValue_def = Define `
 
 val normal_def = Define `
   normal (v:real) (m:mType) =
-    (minValue m <= abs v /\ abs v <= maxValue m)`;
+    (minValue_pos m <= abs v /\ abs v <= maxValue m)`;
 
 val denormal_def = Define `
   denormal (v:real) (m:mType) =
     case m of
-      | M0 => F
-      | _ => ((abs v) < (minValue m) /\ v <> 0)`;
+      | REAL => F
+      | _ => ((abs v) < (minValue_pos m) /\ v <> 0)`;
 
 (**
   Predicate that is true if and only if the given value v is a valid
@@ -176,13 +218,18 @@ val denormal_def = Define `
 val validFloatValue_def = Define `
   validFloatValue (v:real) (m:mType) =
    case m of
-    | M0 => T
+    | REAL => T
     | _ => normal v m \/ denormal v m \/ v = 0`
 
 val validValue_def = Define `
   validValue (v:real) (m:mType) =
     case m of
-      | M0 => T
+      | REAL => T
       | _ => abs v <= maxValue m`;
 
+val no_underflow_fixed_point = store_thm (
+  "no_underflow_fixed_point",
+  ``!v f w. ~ denormal v (F w f)``,
+  fs[denormal_def, minValue_pos_def, REAL_NOT_LT, REAL_ABS_POS]);
+
 val _ = export_theory();

hol4/Infra/RealSimpsScript.sml

@@ -54,6 +54,9 @@ val maxAbs = store_thm ("maxAbs",
   \\ simp [REAL_LE_MAX]
   \\ REAL_ASM_ARITH_TAC);
 
+val maxAbs_def = Define `
+  maxAbs iv = max (abs (FST iv)) (abs (SND iv))`;
+
 val Rabs_err_simpl = store_thm("Rabs_err_simpl",
   ``!(a:real) (b:real). abs (a - (a * (1 + b))) = abs (a * b)``,
   rpt strip_tac \\ REAL_ASM_ARITH_TAC);

hol4/IntervalArithScript.sml

@@ -90,9 +90,6 @@ multInterval (iv1:interval) (iv2:interval) = absIntvUpd ( * ) iv1 iv2`;
 val divideInterval_def = Define `
 divideInterval iv1 iv2 = multInterval iv1 (invertInterval iv2)`;
 
-val maxAbs_def = Define `
-maxAbs iv = max (abs (FST iv)) (abs (SND iv))`;
-
 val minAbsFun_def = Define `
 minAbsFun iv = min (abs (FST iv)) (abs (SND iv))`;
 

hol4/IntervalValidationScript.sml

@@ -142,7 +142,7 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
        vars_typed ((domain fVars) UNION (domain dVars)) Gamma  ==>
        ? iv err vR.
          FloverMapTree_find f A = SOME(iv, err) /\
-         eval_exp E (toRMap Gamma) (toREval f) vR M0 /\
+         eval_exp E (toRMap Gamma) (toREval f) vR REAL /\
          (FST iv) <= vR /\ vR <= (SND iv)``,
   Induct_on `f`
   \\ once_rewrite_tac [usedVars_def, toREval_def] \\ rpt strip_tac
@@ -173,9 +173,7 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
       \\ irule REAL_LE_TRANS \\ asm_exists_tac \\ fs[] \\ rveq \\ fs[])
   (* Const case *)
   >- (qexists_tac `v` \\ fs[]
-      \\ irule Const_dist' \\ fs[]
-      \\ qexists_tac `0` \\ fs[perturb_def]
-      \\ irule mTypeToQ_pos)
+      \\ irule Const_dist' \\ fs[perturb_def, mTypeToR_def])
   (* Unary operator case *)
   >- (first_x_assum (qspecl_then [`A`, `P`, `fVars`, `dVars`, `E`, `Gamma`] destruct)
       \\ fs[]
@@ -185,12 +183,12 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
       >- (qexists_tac `- vR` \\ fs[negateInterval_def, isSupersetInterval_def]
           \\ Cases_on `iv` \\ fs[IVlo_def, IVhi_def]
           \\ rpt conj_tac \\ TRY REAL_ASM_ARITH_TAC
-          \\ irule Unop_neg' \\ qexistsl_tac [`M0`, `vR`] \\ fs[evalUnop_def])
+          \\ irule Unop_neg' \\ qexistsl_tac [`REAL`, `vR`] \\ fs[evalUnop_def])
       (* Inversion case *)
       \\ qexists_tac `1 / vR`
       \\ conj_tac
-      >- (irule Unop_inv' \\ fs[] \\ qexistsl_tac [`0`, `vR`]
-          \\ fs[evalUnop_def, perturb_def, REAL_INV_1OVER, mTypeToQ_pos, IVhi_def, IVlo_def]
+      >- (irule Unop_inv' \\ fs[mTypeToR_def] \\ qexistsl_tac [`vR`]
+          \\ fs[evalUnop_def, mTypeToR_def, perturb_def, REAL_INV_1OVER, mTypeToR_pos, IVhi_def, IVlo_def]
           \\ CCONTR_TAC \\ fs[] \\ rveq
           \\ `0 < 0:real` by (REAL_ASM_ARITH_TAC)
           \\ fs[])
@@ -216,13 +214,13 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
                (qspecl_then [`A`, `P`, `fVars`, `dVars`, `E`, `Gamma`] destruct)
                \\ fs[domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF])
       \\ rveq
-      \\ rename1 `eval_exp E (toRMap Gamma) (toREval f1) vR1 M0`
-      \\ rename1 `eval_exp E (toRMap Gamma) (toREval f2) vR2 M0`
+      \\ rename1 `eval_exp E (toRMap Gamma) (toREval f1) vR1 REAL`
+      \\ rename1 `eval_exp E (toRMap Gamma) (toREval f2) vR2 REAL`
       \\ qexists_tac `evalBinop b vR1 vR2`
       \\ conj_tac
-      >- (irule Binop_dist'
-          \\ qexistsl_tac [`0:real`, `M0`, `M0`, `vR1`, `vR2`]
-          \\ fs[join_def, mTypeToQ_pos, perturb_def]
+      >- (irule Binop_dist' \\ fs[mTypeToR_def]
+          \\ qexistsl_tac [`REAL`, `REAL`, `vR1`, `vR2`]
+          \\ fs[join_def, mTypeToR_pos, perturb_def]
           \\ strip_tac \\ rveq \\ fs[IVlo_def, IVhi_def]
           \\ CCONTR_TAC \\ fs[] \\ rveq
           >- (`0 < 0:real` by (irule REAL_LET_TRANS \\ asm_exists_tac \\ fs[])
@@ -282,7 +280,6 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
                 GSYM REAL_INV_1OVER]
                interval_division_valid)
      \\ qpat_x_assum `!x. _` kall_tac \\ REAL_ASM_ARITH_TAC)
-  (** MARKER **)
   (* FMA case *)