Commit 2239fd58 authored by Heiko Becker's avatar Heiko Becker

Strengthen IEEE validator

parent 01e2ff3b
......@@ -5,7 +5,7 @@
value of an operation may be using its real-valued range +- the error bound.
This soundly proves that the runtime value of the expression must be a valid
normal value according to IEEE 754.
value according to IEEE 754.
**)
open preamble
......@@ -32,18 +32,15 @@ val FPRangeValidator_def = Define `
FPRangeValidator e2 A typeMap
| Unop u e =>
FPRangeValidator e A typeMap
| Downcast m e => FPRangeValidator e A typeMap
| _ => T
in
if (IVlo (iv_e_float) = 0)
then IVhi (iv_e_float) = 0 /\ recRes
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
else
if (0 < IVlo (iv_e_float) \/ IVhi (iv_e_float) < 0)
then
recRes /\
normal (IVlo iv_e_float) m /\
normal (IVhi iv_e_float) m
else
F
F
| NONE => F`;
val enclosure_to_abs = store_thm (
......@@ -89,24 +86,6 @@ val normal_enclosing = store_thm (
\\ fs[]
\\ RealArith.REAL_ASM_ARITH_TAC);
val validFloatValue_enclosing = store_thm (
"validFloatValue_enclosing",
``!v m vHi vLo.
(0 < vLo \/ vHi < 0) /\
(vLo <> 0) /\ (vHi <> 0) /\
validFloatValue vLo m /\
validFloatValue vHi m /\
vLo <= v /\ v <= vHi ==>
validFloatValue v m ``,
rpt gen_tac
\\ disch_then (fn thm => assume_all (CONJ_LIST 6 thm))
\\ `(abs vLo <= abs v /\ abs v <= abs vHi) \/
(abs vHi <= abs v /\ abs v <= abs vLo)`
by (irule enclosure_to_abs \\ fs[])
\\ Cases_on `m` \\ fs[validFloatValue_def] \\ rveq \\ fs[]
\\ DISJ1_TAC
\\ irule normal_enclosing \\ qexistsl_tac [`vHi`, `vLo`] \\ fs[]);
val FPRangeValidator_sound = store_thm (
"FPRangeValidator_sound",
``!e E1 E2 Gamma v m A tMap P fVars dVars.
......@@ -149,13 +128,15 @@ val FPRangeValidator_sound = store_thm (
\\ qspecl_then [`vR`, `v`, `err_e`, `(e_lo,e_hi)`] impl_subgoal_tac (SIMP_RULE std_ss [contained_def, widenInterval_def] distance_gives_iv)
\\ fs[IVlo_def, IVhi_def]
\\ rpt (qpat_x_assum `!x. _` kall_tac)
\\ every_case_tac
\\ rpt (rw_thm_asm `validFloatValue _ _` validFloatValue_def)
\\ fs[widenInterval_def, IVlo_def, IVhi_def]
\\ TRY (`v = 0` by RealArith.REAL_ASM_ARITH_TAC \\ fs[])
\\ DISJ1_TAC
\\ TRY (irule normal_enclosing)
\\ TRY (qexistsl_tac [`e_hi + err_e`, `e_lo - err_e`])
\\ fs[]);
\\ Cases_on `v = 0` \\ TRY(every_case_tac \\ fs[] \\ FAIL_TAC"")
\\ Cases_on `denormal v m` \\ TRY (every_case_tac \\ fs[] \\ FAIL_TAC "")
\\ Cases_on `normal v m` \\ TRY (every_case_tac \\ fs[] \\ FAIL_TAC"")
\\ fs[normal_def, denormal_def, validValue_def] \\ rveq \\ fs[]
\\ TRY (RealArith.REAL_ASM_ARITH_TAC)
\\ every_case_tac \\ fs[]
\\ `abs v <= abs (FST (widenInterval (e_lo, e_hi) err_e)) \/
abs v <= abs (SND (widenInterval (e_lo, e_hi) err_e))`
by (fs[widenInterval_def, IVlo_def, IVhi_def] \\ RealArith.REAL_ASM_ARITH_TAC)
\\ every_case_tac \\ RealArith.REAL_ASM_ARITH_TAC);
val _ = export_theory();
......@@ -178,6 +178,16 @@ 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.
......@@ -188,6 +198,6 @@ val validFloatValue_def = Define `
validFloatValue (v:real) (m:mType) =
case m of
| M0 => T
| _ => normal v m \/ v = 0`
| _ => normal v m \/ denormal v m \/ v = 0`
val _ = export_theory();
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