Commit d945a600 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'master' into IEEE_connection

parents baa560ad 6f0f0bd3
......@@ -42,7 +42,7 @@ val add_abs_err_bounded = store_thm ("add_abs_err_bounded",
\\ rename1 `vR = perturb (evalBinop Plus v1R v2R) deltaR`
\\ inversion `eval_exp _ _ (Binop Plus (Var 1) (Var 2)) _ _` eval_exp_cases
\\ rename1 `vF = perturb (evalBinop Plus v1F v2F) deltaF`
\\ `(m1' = M0) /\ (m2' = M0)` by (match_mp_tac M0_join_is_M0 \\ fs[]) \\ fs []
\\ `(m1' = M0) /\ (m2' = M0)` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs[]) \\ fs []
\\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
\\ `perturb (evalBinop Plus v1R v2R) deltaR = evalBinop Plus v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[])
\\ `vR = evalBinop Plus v1R v2R` by simp[]
......@@ -87,7 +87,7 @@ val subtract_abs_err_bounded = store_thm ("subtract_abs_err_bounded",
\\ rename1 `vR = perturb (evalBinop Sub v1R v2R) deltaR`
\\ inversion `eval_exp _ _ (Binop Sub (Var 1) (Var 2)) _ _` eval_exp_cases
\\ rename1 `vF = perturb (evalBinop Sub v1F v2F) deltaF`
\\ `(m1' = M0) /\ (m2' = M0)` by (match_mp_tac M0_join_is_M0 \\ fs[]) \\ fs []
\\ `(m1' = M0) /\ (m2' = M0)` by (conj_tac \\ irule toRMap_eval_M0\\ asm_exists_tac \\ fs[]) \\ fs []
\\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
\\ `perturb (evalBinop Sub v1R v2R) deltaR = evalBinop Sub v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[])
\\ `vR = evalBinop Sub v1R v2R` by simp[]
......@@ -136,7 +136,7 @@ val mult_abs_err_bounded = store_thm ("mult_abs_err_bounded",
\\ rename1 `vR = perturb (evalBinop Mult v1R v2R) deltaR`
\\ inversion `eval_exp _ _ (Binop Mult (Var 1) (Var 2)) _ _` eval_exp_cases
\\ rename1 `vF = perturb (evalBinop Mult v1F v2F) deltaF`
\\ `(m1' = M0) /\ (m2' = M0)` by (match_mp_tac M0_join_is_M0 \\ fs[]) \\ fs []
\\ `(m1' = M0) /\ (m2' = M0)` by (conj_tac \\ irule toRMap_eval_M0\\ asm_exists_tac \\ fs[]) \\ fs []
\\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
\\ `perturb (evalBinop Mult v1R v2R) deltaR = evalBinop Mult v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[])
\\ `vR = evalBinop Mult v1R v2R` by simp[]
......@@ -178,7 +178,7 @@ val div_abs_err_bounded = store_thm ("div_abs_err_bounded",
\\ rename1 `vR = perturb (evalBinop Div v1R v2R) deltaR`
\\ inversion `eval_exp _ _ (Binop Div (Var 1) (Var 2)) _ _` eval_exp_cases
\\ rename1 `vF = perturb (evalBinop Div v1F v2F) deltaF`
\\ `(m1' = M0) /\ (m2' = M0)` by (match_mp_tac M0_join_is_M0 \\ fs[]) \\ fs []
\\ `(m1' = M0) /\ (m2' = M0)` by (conj_tac \\ irule toRMap_eval_M0\\ asm_exists_tac \\ fs[]) \\ fs []
\\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
\\ `perturb (evalBinop Div v1R v2R) deltaR = evalBinop Div v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[])
\\ `vR = evalBinop Div v1R v2R` by simp[]
......
......@@ -2267,7 +2267,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
\\ rw_thm_asm `eval_exp E1 _ _ _ _` toREval_def
\\ fs[]
\\ inversion `eval_exp E1 _ _ _ _` eval_exp_cases
\\ `m1 = M0 /\ m2 = M0` by (metis_tac [M0_join_is_M0])
\\ `m1 = M0 /\ m2 = M0` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs[])
\\ rveq
\\ `(?nF1 m1. eval_exp E2 Gamma e1 nF1 m1) /\
(!nF1 m1. eval_exp E2 Gamma e1 nF1 m1 ==> abs (v1 - nF1) <= err_e1)`
......
(**
Some abbreviations that require having defined expressions beforehand
If we would put them in the Abbrevs file, this would create a circular dependency which Coq cannot resolve.
If we would put them in the Abbrevs file, this would create a circular dependency which HOL4 cannot resolve.
**)
open preamble
open ExpressionsTheory
......
......@@ -54,13 +54,13 @@ val _ = Datatype `
| Downcast mType exp`
val toREval_def = Define `
toREval (e:real exp) : real exp =
toREval e :real exp =
case e of
| Var n => Var n
| Const m n => Const M0 n
| Unop u e1 => Unop u (toREval e1)
| Binop bop e1 e2 => Binop bop (toREval e1) (toREval e2)
| Downcast m e1 => (toREval e1)`;
| (Var n) => Var n
| (Const m n) => Const M0 n
| (Unop u e1) => Unop u (toREval e1)
| (Binop bop e1 e2) => Binop bop (toREval e1) (toREval e2)
| (Downcast m e1) => (toREval e1)`;
(**
Define a perturbation function to ease writing of basic definitions
......@@ -205,13 +205,32 @@ val delta_M0_deterministic = store_thm("delta_M0_deterministic",
``!(v:real) (delta:real). abs delta <= mTypeToQ M0 ==> perturb v delta = v``,
fs [mTypeToQ_def,perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]);
val toRMap_def = Define `
toRMap (d:num -> mType option) (n:num) : mType option =
case d n of
| SOME m => SOME M0
| NONE => NONE`;
val toRMap_eval_M0 = store_thm (
"toRMap_eval_M0",
``!f v E Gamma m.
eval_exp E (toRMap Gamma) (toREval f) v m ==> m = M0``,
Induct \\ simp[Once toREval_def] \\ fs[eval_exp_cases, toRMap_def]
\\ rpt strip_tac \\ fs[]
>- (every_case_tac \\ fs[])
>- (rveq \\ first_x_assum drule \\ strip_tac \\ fs[])
>- (rveq \\ first_x_assum drule \\ strip_tac \\ fs[])
>- (`m1 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[])
\\ `m2 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[])
\\ rveq \\ fs[join_def]));
(**
Evaluation with 0 as machine epsilon is deterministic
**)
val meps_0_deterministic = store_thm("meps_0_deterministic",
``!(f: real exp) v1:real v2:real E defVars.
eval_exp E defVars (toREval f) v1 M0 /\
eval_exp E defVars (toREval f) v2 M0 ==>
eval_exp E (toRMap defVars) (toREval f) v1 M0 /\
eval_exp E (toRMap defVars) (toREval f) v2 M0 ==>
v1 = v2``,
Induct_on `f`
>- (rw [toREval_def] \\ fs [eval_exp_cases])
......@@ -231,13 +250,13 @@ val meps_0_deterministic = store_thm("meps_0_deterministic",
qpat_x_assum `eval_exp _ _ (toREval _) _ _`
(fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm)))
\\ Cases_on `b` \\ fs [eval_exp_cases]
\\ `m1 = M0 /\ m2 = M0` by (match_mp_tac M0_join_is_M0 \\ fs [])
\\ `m1 = M0 /\ m2 = M0` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs [])
\\ rw[]
\\ rename1 `eval_exp E _ (toREval f1) vf11 M0`
\\ rename1 `eval_exp E _ (toREval f1) vf12 m1`
\\ rename1 `eval_exp E _ (toREval f2) vf21 M0`
\\ rename1 `eval_exp _ _ (toREval f2) vf22 m2`
\\ `m1 = M0 /\ m2 = M0` by (match_mp_tac M0_join_is_M0 \\ fs [])
\\ `m1 = M0 /\ m2 = M0` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs [])
\\ rw []
\\ fs [join_def, mTypeToQ_def, delta_0_deterministic]
\\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`vf21`,`vf22`] ASSUME_TAC thm)
......@@ -246,17 +265,11 @@ val meps_0_deterministic = store_thm("meps_0_deterministic",
\\ rw[])
>- (rw[]
\\ rpt (
qpat_x_assum `eval_exp _ _ (toREval _) _ _`
qpat_x_assum `eval_exp _ _ (toREval (Downcast _ _)) _ _`
(fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm)))
\\ fs [eval_exp_cases]
\\ res_tac));
val toRMap_def = Define `
toRMap (d:num -> mType option) (n:num) : mType option =
case d n of
| SOME m => SOME M0
| NONE => NONE`;
(**
Helping lemma. Needed in soundness proof.
For each evaluation of using an arbitrary epsilon, we can replace it by
......
......@@ -10,18 +10,19 @@ open realTheory realLib sptreeTheory
val _ = new_theory "MachineType";
val _ = Datatype `
mType = M0 | M32 | M64 | M128 | M256`;
mType = M0 | M16 | M32 | M64(* | M128 | M256 *)`;
val mTypeToQ_def = Define `
mTypeToQ (m:mType) : real =
case m of
| M0 => 0
| M16 => 1 / (2 pow 11)
| M32 => 1 / (2 pow 24)
| M64 => 1 / (2 pow 53)
(* the epsilons below match what is used internally in daisy,
although these value do not match the IEEE standard *)
| M128 => 1 / (2 pow 105)
| M256 => 1 / (2 pow 211)`;
(* | M128 => 1 / (2 pow 105) *)
(* | M256 => 1 / (2 pow 211) *)`;
val meps_def = Define `meps = mTypeToQ`;
......@@ -59,20 +60,78 @@ val M0_lower_bound = store_thm ("M0_lower_bound",
**)
val join_def = Define `
join (m1:mType) (m2:mType) =
if (isMorePrecise m1 m2) then m2 else m1`;
if (isMorePrecise m1 m2) then m1 else m2`;
(* val M0_join_is_M0 = store_thm ("M0_join_is_M0", *)
(* ``!m1 m2. *)
(* join m1 m2 = M0 ==> *)
(* (m1 = M0 /\ m2 = M0)``, *)
(* 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` *)
(* (fn thm => fs [thm]) *)
(* >- (Cases_on `m1` \\ fs [mTypeToQ_def]) *)
(* >- (Cases_on `m2` \\ fs [mTypeToQ_def])); *)
val M0_join_is_M0 = store_thm ("M0_join_is_M0",
``!m1 m2.
join m1 m2 = M0 ==>
(m1 = M0 /\ m2 = M0)``,
fs [join_def, isMorePrecise_def] \\
rpt strip_tac \\
Cases_on `mTypeToQ m1 <= mTypeToQ m2` \\
fs [] \\
qpat_x_assum `_ = M0`
(fn thm => fs [thm])
>- (Cases_on `m1` \\ fs [mTypeToQ_def])
>- (Cases_on `m2` \\ fs [mTypeToQ_def]));
val maxExponent_def = Define `
(maxExponent (M0) = 0n) /\
(maxExponent (M16) = 15) /\
(maxExponent (M32) = 127) /\
(maxExponent (M64) = 1023)
(* | M128 => 1023 (** FIXME **) *)
(* | M256 => 1023 *)`;
val minExponentPos_def = Define `
(minExponentPos (M0) = 0n) /\
(minExponentPos (M16) = 14) /\
(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`;
(** 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)))`;
(** 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)`;
(**
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 \/ v = 0`
val maxExponent_def = Define `
maxExponent (m:mType) :num=
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment