Start working on coq port

coq/FPRangeValidator.v

+
+(* TODO: Flocq ops open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory *)
+
+Require Import Daisy.Infra.MachineType Daisy.Typing Daisy.Infra.RealSimps Daisy.CertificateChecker.
+
+Fixpoint FPRangeValidator (e:exp Q) A typeMap dVars {struct e} : bool :=
+  match typeMap e with
+  |Some m =>
+        let (iv_e, err_e) := A e in
+        let iv_e_float := widenInterval iv_e err_e in
+        let recRes :=
+            match e with
+            | Binop b e1 e2 =>
+              FPRangeValidator e1 A typeMap dVars /\
+              FPRangeValidator e2 A typeMap dVars
+            | Unop u e =>
+              FPRangeValidator e A typeMap dVars
+            | Downcast m e => FPRangeValidator e A typeMap dVars
+            | _ =>  true
+            end
+        in
+        match e with
+        | Var _ v =>
+          if NatSet.mem v dVars
+          then true
+          else
+            if (validValue (IVhi iv_e_float) m /\
+                validValue (IVlo iv_e_float) m)
+            then ((normal (IVlo iv_e_float) m) \/ ((IVlo iv_e_float) = 0) \/
+                  normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0) /\ recRes
+            else
+              false
+        | _ => if (validValue (IVhi iv_e_float) m /\
+                  validValue (IVlo iv_e_float) m)
+              then ((normal (IVlo iv_e_float) m) \/ ((IVlo iv_e_float) = 0) \/
+                    normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0) /\ recRes
+              else
+                false
+        end
+  | None => false
+  end.
+      | SOME m =>
+
+      | NONE => F`;
+  .
+
+open AbbrevsTheory MachineTypeTheory TypingTheory RealSimpsTheory IntervalArithTheory
+     ExpressionsTheory DaisyTactics IntervalValidationTheory ErrorValidationTheory
+     CommandsTheory EnvironmentsTheory ssaPrgsTheory
\ No newline at end of file

coq/Infra/MachineType.v

@@ -11,7 +11,7 @@ Require Import Daisy.Infra.RealRationalProps.
 (**
    Define machine precision as datatype
  **)
-Inductive mType: Type := M0 | M32 | M64 | M128 | M256.
+Inductive mType: Type := M0 | M16 | M32 | M64. (*| M128 | M256*)
 
 (**
   Injection of machine types into Q
@@ -19,12 +19,14 @@ Inductive mType: Type := M0 | M32 | M64 | M128 | M256.
 Definition mTypeToQ (e:mType) :Q :=
   match e with
   | M0 => 0
+  | M16 => (Qpower (2#1) (Zneg 11))
   | M32 => (Qpower (2#1) (Zneg 24))
   | M64 => (Qpower (2#1) (Zneg 53))
+  (*
   (* the epsilons below match what is used internally in daisy,
   although these value do not match the IEEE standard *)
   | M128 => (Qpower (2#1) (Zneg 105))
-  | M256 => (Qpower (2#1) (Zneg 211))
+  | M256 => (Qpower (2#1) (Zneg 211)) *)
   end.
 
 Arguments mTypeToQ _/.
@@ -49,10 +51,11 @@ Qed.
 Definition mTypeEq (m1:mType) (m2:mType) :=
   match m1, m2 with
   | M0, M0 => true
+  | M16, M16 => true
   | M32, M32 => true
   | M64, M64 => true
-  | M128, M128 => true
-  | M256, M256 => true
+  (* | M128, M128 => true *)
+  (* | M256, M256 => true *)
   | _, _ => false
   end.
 
@@ -141,4 +144,59 @@ Definition join (m1:mType) (m2:mType) :=
 (*   unfold join. *)
 (*   intros. *)
 (*   destruct m1, m2; simpl in *; cbv in *; try congruence; try auto. *)
-(* Qed. *)
\ No newline at end of file
+(* Qed. *)
+
+Definition maxExponent (m:mType) :Z :=
+  match m with
+  | M0 => 0
+  | M16 => 15
+  | M32 => 127
+  | M64 => 1023
+  end.
+
+Definition minExponentPos (m:mType) :Z :=
+  match m with
+  | M0 => 0
+  | M16 => 14
+  | M32 => 126
+  | M64 => 1022
+  end.
+
+(**
+Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
+(𝛃 - 𝛃^(1 - p)) * 𝛃^(e_max)
+
+which simplifies to 2^(e_max) for base 2
+**)
+Definition maxValue (m:mType) :=
+  Qpower (2#1) (maxExponent m).
+
+Definition minValue (m:mType) :=
+  Qinv (Qpower (2#1) (minExponentPos m)).
+
+(** Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
+  𝛃^(e_min -p + 1) = 𝛃^(e_min -1) for base 2
+**)
+Definition minDenormalValue (m:mType) :=
+  Qinv (Qpower (2#1) (minExponentPos m - 1)).
+
+Definition normal (v:Q) (m:mType) :=
+  Qle_bool (minValue m) (Qabs v) && Qle_bool (Qabs v) (maxValue m).
+
+(**
+  Predicate that is true if and only if the given value v is a valid
+  floating-point value according to the the type m.
+  Since we use the 1 + 𝝳 abstraction, the value must either be
+  in normal range or 0.
+**)
+Definition validFloatValue (v:Q) (m:mType) :=
+  match m with
+  | M0 => true
+  | _ => normal v m || Qeq_bool v 0
+  end.
+
+Definition validValue (v:Q) (m:mType) :=
+  match m with
+  | M0 => true
+  | _ => Qle_bool (Qabs v) (maxValue m)
+  end.
\ No newline at end of file

hol4/Infra/MachineTypeScript.sml

@@ -117,7 +117,7 @@ val minValue_def = Define `
 **)
 
 val minDenormalValue_def = Define `
-  minDenormalValue (m:mType) = 1 / (2 pow (minExponentPos m))`;
+  minDenormalValue (m:mType) = 1 / (2 pow (minExponentPos m - 1))`;
 
 val normal_def = Define `
   normal (v:real) (m:mType) =
@@ -135,67 +135,10 @@ val validFloatValue_def = Define `
     | M0 => T
     | _ => normal v m \/ v = 0`
 
-val maxExponent_def = Define `
-  maxExponent (m:mType) :num=
-    case m of
-     | M0 => 0
-     | M32 => 127
-     | M64 => 1023
-     | M128 => 1023 (** FIXME **)
-     | M256 => 1023`;
-
-val minExponentPos_def = Define `
-  (minExponentPos (M0) = 0n) /\
-  (minExponentPos (M32) = 126) /\
-  (minExponentPos (M64) = 1022) /\
-  (minExponentPos (M128) = 1022) /\ (* FIXME *)
-  (minExponentPos (M256) = 1022)`;
-
-(**
-Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
-(𝛃 - 𝛃^(1 - p)) * 𝛃^(e_max)
-
-which simplifies to 2^(e_max) for base 2
-**)
-
-val maxValue_def = Define `
-  maxValue (m:mType) = (&(2n ** (maxExponent m))):real`;
-
-val minValue_def = Define `
- minValue (m:mType) = inv (&(2n ** (minExponentPos m)))`;
-
-
-(** Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
-  𝛃^(e_min -p + 1) = 𝛃^(e_min -1) for base 2
-**)
-
-val minDenormalValue_def = Define `
-  minDenormalValue (m:mType) = 1 / (2 pow (minExponentPos m))`;
-
-val normal_def = Define `
-  normal (v:real) (m:mType) =
-    (minValue m <= abs v /\ abs v <= maxValue m)`;
-
-val denormal_def = Define `
-  denormal (v:real) (m:mType) =
-    ((abs v) < (minValue m) /\ v <> 0)`;
-
 val validValue_def = Define `
   validValue (v:real) (m:mType) =
     case m of
       | M0 => T
       | _ => abs v <= maxValue m`;
 
-(**
-  Predicate that is true if and only if the given value v is a valid
-  floating-point value according to the the type m.
-  Since we use the 1 + 𝝳 abstraction, the value must either be
-  in normal range or 0.
-**)
-val validFloatValue_def = Define `
-  validFloatValue (v:real) (m:mType) =
-   case m of
-    | M0 => T
-    | _ => normal v m \/ denormal v m \/ v = 0`
-
 val _ = export_theory();