Commit e7cc1ef7 authored by Heiko Becker's avatar Heiko Becker

Fix fixed-point implementation in HOL4 development

parent 313ac660
......@@ -16,10 +16,10 @@ val _ = temp_overload_on("abs",``real$abs``);
(** Certificate checking function **)
val CertificateChecker_def = Define
`CertificateChecker (e:real exp) (A:analysisResult) (P:precond)
(defVars: num -> mType option) =
let tMap = typeMap defVars e FloverMapTree_empty in
if (typeCheck e defVars tMap) then
`CertificateChecker (e:real expr) (A:analysisResult) (P:precond)
(defVars: num -> mType option) (fBits:bitMap) =
let tMap = typeMap defVars e FloverMapTree_empty fBits in
if (typeCheck e defVars tMap fBits) then
if (validIntervalbounds e A P LN /\
FPRangeValidator e A tMap LN)
then (validErrorbound e tMap A LN)
......@@ -32,7 +32,7 @@ val CertificateChecker_def = Define
the real valued execution respects the precondition.
**)
val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
``!(e:real exp) (A:analysisResult) (P:precond) (E1 E2:env) defVars fVars.
``!(e:real expr) (A:analysisResult) (P:precond) (E1 E2:env) defVars fVars fBits.
approxEnv E1 defVars A fVars LN E2 /\
(!v.
v IN (domain fVars) ==>
......@@ -41,13 +41,13 @@ val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
FST (P v) <= vR /\ vR <= SND (P v)) /\
(domain (usedVars e)) SUBSET (domain fVars) /\
(!v. v IN domain fVars ==> ?m. defVars v = SOME m) /\
CertificateChecker e A P defVars ==>
CertificateChecker e A P defVars fBits ==>
?iv err vR vF m.
FloverMapTree_find e A = SOME (iv,err) /\
eval_exp E1 (toRMap defVars) (toREval e) vR REAL /\
eval_exp E2 defVars e vF m /\
eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval e) vR REAL /\
eval_expr E2 defVars (toRBMap fBits) e vF m /\
(!vF m.
eval_exp E2 defVars e vF m ==>
eval_expr E2 defVars (toRBMap fBits) e vF m ==>
abs (vR - vF) <= err /\ validFloatValue vF m)``,
(**
The proofs is a simple composition of the soundness proofs for the range
......@@ -57,7 +57,7 @@ val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
\\ rpt strip_tac
\\ drule validIntervalbounds_sound
\\ rpt (disch_then drule)
\\ disch_then (qspecl_then [`fVars`,`E1`, `defVars`] destruct)
\\ disch_then (qspecl_then [`fVars`,`E1`, `defVars`, `toRBMap fBits`] destruct)
\\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]
\\ drule validErrorbound_sound
\\ rpt (disch_then drule)
......@@ -74,9 +74,9 @@ val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
val CertificateCheckerCmd_def = Define
`CertificateCheckerCmd (f:real cmd) (absenv:analysisResult) (P:precond)
defVars =
let tMap = typeMapCmd defVars f FloverMapTree_empty in
if (typeCheckCmd f defVars tMap /\
defVars fBits =
let tMap = typeMapCmd defVars f FloverMapTree_empty fBits in
if (typeCheckCmd f defVars tMap fBits /\
validSSA f (freeVars f))
then
if ((validIntervalboundsCmd f absenv P LN) /\
......@@ -87,7 +87,7 @@ val CertificateCheckerCmd_def = Define
val CertificateCmd_checking_is_sound = store_thm ("CertificateCmd_checking_is_sound",
``!(f:real cmd) (A:analysisResult) (P:precond) defVars
(E1 E2:env) (fVars:num_set).
(E1 E2:env) (fVars:num_set) fBits.
approxEnv E1 defVars A (freeVars f) LN E2 /\
(!v.
v IN (domain (freeVars f)) ==>
......@@ -96,30 +96,30 @@ val CertificateCmd_checking_is_sound = store_thm ("CertificateCmd_checking_is_so
FST (P v) <= vR /\ vR <= SND (P v)) /\
domain (freeVars f) SUBSET (domain fVars) /\
(!v. v IN domain (freeVars f) ==> ?m. defVars v = SOME m) /\
CertificateCheckerCmd f A P defVars ==>
CertificateCheckerCmd f A P defVars fBits ==>
?iv err vR vF m.
FloverMapTree_find (getRetExp f) A = SOME (iv, err) /\
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)``,
bstep (toREvalCmd f) E1 (toRMap defVars) (toRBMap fBits) vR REAL /\
bstep f E2 defVars (toRBMap fBits) vF m /\
(!vF m. bstep f E2 defVars (toRBMap fBits) vF m ==> abs (vR - vF) <= err)``,
simp [CertificateCheckerCmd_def]
\\ rpt strip_tac
\\ `?outVars. ssa f (freeVars f) outVars` by (match_mp_tac validSSA_sound \\ fs[])
\\ qspecl_then
[`f`, `A`, `E1`, `freeVars f`, `LN`, `outVars`, `P`, `defVars`]
[`f`, `A`, `E1`, `freeVars f`, `LN`, `outVars`, `P`, `defVars`, `toRBMap fBits`]
destruct validIntervalboundsCmd_sound
\\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]
\\ qspecl_then
[`f`, `A`, `E1`, `E2`, `outVars`, `freeVars f`, `LN`, `vR`, `FST iv`,
`SND iv`, `err`, `P`, `m`, `typeMapCmd defVars f FloverMapTree_empty`,
`defVars`]
`SND iv`, `err`, `P`, `m`, `typeMapCmd defVars f FloverMapTree_empty fBits`,
`defVars`, `fBits`]
destruct validErrorboundCmd_gives_eval
\\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]
\\ rpt (asm_exists_tac \\ fs[])
\\ rpt strip_tac
\\ drule validErrorboundCmd_sound
\\ rpt (disch_then drule)
\\ rename1 `bstep f E2 defVars vF2 m2`
\\ rename1 `bstep f E2 defVars (toRBMap fBits) vF2 m2`
\\ disch_then (qspecl_then
[`outVars`, `vR`, `vF2`, `FST iv`, `SND iv`, `err`, `P`,`m2`] destruct)
\\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]);
......
......@@ -13,9 +13,8 @@ val _ = new_theory "Commands";
Only assignments and return statement
**)
val _ = Datatype `
cmd = Let mType num ('v exp) cmd
| Ret ('v exp)`;
cmd = Let mType num ('v expr) cmd
| Ret ('v expr)`;
val toREvalCmd_def = Define `
toREvalCmd (f:real cmd) : real cmd =
......@@ -28,21 +27,21 @@ val toREvalCmd_def = Define `
result value
**)
val (bstep_rules, bstep_ind, bstep_cases) = Hol_reln `
(!m m' x e s E v res Gamma.
eval_exp E Gamma e v m /\
bstep s (updEnv x v E) (updDefVars x m Gamma) res m' ==>
bstep (Let m x e s) E Gamma res m') /\
(!m e E v Gamma.
eval_exp E Gamma e v m ==>
bstep (Ret e) E Gamma v m)`;
(!m m' x e s E v res Gamma fBits.
eval_expr E Gamma fBits e v m /\
bstep s (updEnv x v E) (updDefVars x m Gamma) fBits res m' ==>
bstep (Let m x e s) E Gamma fBits res m') /\
(!m e E v Gamma fBits.
eval_expr E Gamma fBits e v m ==>
bstep (Ret e) E Gamma fBits v m)`;
(**
Generate a better case lemma again
**)
val bstep_cases =
map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bstep_cases])
[``bstep (Let m x e s) E defVars vR m'``,
``bstep (Ret e) E defVars vR m``]
[``bstep (Let m x e s) E defVars fBits vR m'``,
``bstep (Ret e) E defVars fBits vR m``]
|> LIST_CONJ |> curry save_thm "bstep_cases";
val [let_b, ret_b] = CONJ_LIST 2 bstep_rules;
......@@ -50,7 +49,7 @@ save_thm ("let_b", let_b);
save_thm ("ret_b", ret_b);
(**
The free variables of a command are all used variables of expressions
The free variables of a command are all used variables of exprressions
without the let bound variables
**)
val freeVars_def = Define `
......@@ -70,10 +69,10 @@ val definedVars_def = Define `
val bstep_eq_env = store_thm (
"bstep_eq_env",
``!f E1 E2 Gamma v m.
``!f E1 E2 Gamma v m fBits.
(!x. E1 x = E2 x) /\
bstep f E1 Gamma v m ==>
bstep f E2 Gamma v m``,
bstep f E1 Gamma fBits v m ==>
bstep f E2 Gamma fBits v m``,
Induct \\ rpt strip_tac \\ fs[bstep_cases]
>- (qexists_tac `v'` \\ conj_tac
\\ TRY (drule eval_eq_env \\ disch_then drule \\ fs[] \\ FAIL_TAC"")
......
This diff is collapsed.
This diff is collapsed.
(**
Some abbreviations that require having defined expressions beforehand
Some abbreviations that require having defined exprressions beforehand
If we would put them in the Abbrevs file, this would create a circular dependency which HOL4 cannot resolve.
**)
open ExpressionsTheory
open FloverMapTheory
open preamble
val _ = new_theory "ExpressionAbbrevs"
val _ = new_theory "ExpressionAbbrevs";
(**
We treat a function mapping an expression arguing on fractions as value type
We treat a function mapping an exprression arguing on fractions as value type
to pairs of intervals on rationals and rational errors as the analysis result
**)
(* val _ = type_abbrev("analysisResult", ``:real exp->(interval # real)``); *)
val _ = type_abbrev ("typeMap", ``:(real expr # mType) binTree``);
val _ = type_abbrev ("bitMap", ``:(real expr # num) binTree``);
val _ = type_abbrev ("analysisResult", ``:(real expr # ((real # real) # real)) binTree``);
val toRBMap_def = Define `
toRBMap (fBits:bitMap) =
\e. FloverMapTree_find e fBits`;
val _ = export_theory()
This diff is collapsed.
......@@ -4,7 +4,7 @@
The Floating-Point range validator computes an overapproximation of what the
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
This soundly proves that the runtime value of the exprression must be a valid
value according to IEEE 754.
**)
......@@ -19,7 +19,7 @@ val _ = new_theory "FPRangeValidator";
val _ = temp_overload_on("abs",``real$abs``);
val FPRangeValidator_def = Define `
FPRangeValidator (e:real exp) A typeMap dVars =
FPRangeValidator (e:real expr) A typeMap dVars =
case FloverMapTree_find e A, FloverMapTree_find e typeMap of
| SOME (iv_e, err_e), SOME m =>
let iv_e_float = widenInterval iv_e err_e in
......@@ -119,7 +119,7 @@ val solve_tac =
\\ 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[]
\\ fs[normal_def, denormal_def, validFloatValue_def, validValue_def] \\ rveq \\ fs[]
\\ every_case_tac \\ fs[]
\\ `abs v <= abs (FST (widenInterval iv_e err_e)) \/
abs v <= abs (SND (widenInterval iv_e err_e))`
......@@ -128,10 +128,10 @@ val solve_tac =
val FPRangeValidator_sound = store_thm (
"FPRangeValidator_sound",
``!e E1 E2 Gamma v m A tMap P fVars (dVars:num_set).
``!e E1 E2 Gamma v m A tMap P fVars (dVars:num_set) fBits.
approxEnv E1 Gamma A fVars dVars E2 /\
eval_exp E2 Gamma e v m /\
typeCheck e Gamma tMap /\
eval_expr E2 Gamma (toRBMap fBits) e v m /\
typeCheck e Gamma tMap fBits /\
validIntervalbounds e A P dVars /\
validErrorbound e tMap A dVars /\
FPRangeValidator e A tMap dVars /\
......@@ -150,10 +150,10 @@ 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 REAL /\
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval e) vR REAL /\
FST iv <= vR /\ vR <= SND iv`
by (drule validIntervalbounds_sound
\\ disch_then (qspecl_then [`fVars`, `E1`, `Gamma`] impl_subgoal_tac)
\\ disch_then (qspecl_then [`fVars`, `E1`, `Gamma`, `toRBMap fBits`] impl_subgoal_tac)
\\ fs[] \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ qexists_tac `vR` \\ fs[])
\\ rename1 `FloverMapTree_find e A = SOME (iv_e, err_e)` \\ fs[]
......@@ -174,19 +174,19 @@ val FPRangeValidator_sound = store_thm (
by (drule typingSoundnessExp \\ rpt (disch_then drule)
\\ fs[])
\\ fs[] \\ rveq
\\ rpt (inversion `eval_exp E2 _ _ _ _` eval_exp_cases)
\\ rpt (inversion `eval_expr E2 _ _ _ _ _` eval_expr_cases)
\\ qpat_x_assum `E2 n = SOME v` (fn thm => fs[thm]))
\\ solve_tac)
\\ solve_tac);
val FPRangeValidatorCmd_sound = store_thm (
"FPRangeValidatorCmd_sound",
``!f E1 E2 Gamma v vR m A tMap P fVars dVars outVars.
``!f E1 E2 Gamma v vR m A tMap P fVars dVars outVars fBits.
approxEnv E1 Gamma A fVars dVars E2
ssa f (union fVars dVars) outVars /\
bstep (toREvalCmd f) E1 (toRMap Gamma) vR m /\
bstep f E2 Gamma v m
typeCheckCmd f Gamma tMap
bstep (toREvalCmd f) E1 (toRMap Gamma) (toRBMap fBits) vR m /\
bstep f E2 Gamma (toRBMap fBits) v m
typeCheckCmd f Gamma tMap fBits
validIntervalboundsCmd f A P dVars
validErrorboundCmd f tMap A dVars
FPRangeValidatorCmd f A tMap dVars
......@@ -206,9 +206,9 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ Flover_compute ``validIntervalboundsCmd``
\\ Flover_compute ``typeCheckCmd``
\\ rveq \\ fs[]
\\ rpt (inversion `bstep (Let _ _ _ _) _ _ _ _` bstep_cases)
\\ rename1 `bstep (toREvalCmd f) (updEnv n vR_e E1) _ _ mR`
\\ rename1 `bstep f (updEnv n vF E2) _ _ mF`
\\ rpt (inversion `bstep (Let _ _ _ _) _ _ _ _ _` bstep_cases)
\\ rename1 `bstep (toREvalCmd f) (updEnv n vR_e E1) _ _ _ mR`
\\ rename1 `bstep f (updEnv n vF E2) _ _ _ mF`
\\ `FloverMapTree_find e tMap = SOME m`
by (drule typingSoundnessExp
\\ rpt (disch_then drule)
......@@ -227,7 +227,7 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ fs[]
\\ drule validIntervalbounds_sound
\\ rpt (disch_then drule)
\\ disch_then (qspecl_then [`fVars`, `Gamma`] impl_subgoal_tac)
\\ disch_then (qspecl_then [`fVars`, `Gamma`, `toRBMap fBits`] impl_subgoal_tac)
>- (fs[]
\\ fs[DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule
\\ fs[domain_union]
......@@ -241,7 +241,7 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ first_x_assum
(qspecl_then [`updEnv n vR_e E1`, `updEnv n vF E2`,
`updDefVars n m Gamma`, `v`, `vR`, `mF`, `A`, `tMap`, `P`,
`fVars`, `insert n () dVars`, `outVars`]
`fVars`, `insert n () dVars`, `outVars`, `fBits`]
impl_subgoal_tac)
>- (fs[] \\ rpt conj_tac
>- (irule approxUpdBound \\ fs[lookup_NONE_domain]
......@@ -279,7 +279,7 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ TOP_CASE_TAC \\ rveq \\ fs[])
\\ rpt strip_tac
\\ fs[updEnv_def] \\ rveq \\ fs[]
>- (qpat_x_assum `eval_exp E2 Gamma e nF _` kall_tac
>- (qpat_x_assum `eval_expr E2 Gamma _ e nF _` kall_tac
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ disch_then irule \\ fs[]
......@@ -292,7 +292,7 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ first_x_assum (qspec_then `n` assume_tac)
\\ res_tac)
\\ TOP_CASE_TAC \\ fs[]
\\ qpat_x_assum `eval_exp E2 Gamma e nF _` kall_tac
\\ qpat_x_assum `eval_expr E2 Gamma _ e nF _` kall_tac
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ disch_then irule \\ fs[]
......@@ -309,7 +309,7 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ Flover_compute ``validIntervalboundsCmd``
\\ Flover_compute ``typeCheckCmd``
\\ rveq \\ fs[]
\\ rpt (inversion `bstep (Ret _) _ _ _ _` bstep_cases)
\\ rpt (inversion `bstep (Ret _) _ _ _ _ _` bstep_cases)
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ fs[]);
......
open MachineTypeTheory ExpressionAbbrevsTheory FloverTactics
open MachineTypeTheory ExpressionsTheory FloverTactics
open preamble
val _ = new_theory "FloverMap";
......@@ -6,8 +6,8 @@ val _ = new_theory "FloverMap";
val _ = Datatype `
cmp = Lt | Eq | Gt`;
val expCompare_def = Define `
expCompare (e1:real exp) e2 =
val exprCompare_def = Define `
exprCompare (e1:real expr) e2 =
case e1, e2 of
|(Var (n1:num)), (Var n2) =>
if (n1 < n2)
......@@ -28,7 +28,7 @@ val expCompare_def = Define `
| Const _ _, _ => Lt
| Unop u1 e1, Unop u2 e2 =>
if u1 = u2
then expCompare e1 e2
then exprCompare e1 e2
else (if u1 = Neg then Lt else Gt)
| Unop _ _, Binop _ _ _ => Lt
| Unop _ _, Downcast _ _ => Lt
......@@ -36,7 +36,7 @@ val expCompare_def = Define `
| Unop _ _, _ => Gt
| Downcast m1 e1, Downcast m2 e2 =>
if m1 = m2
then expCompare e1 e2
then exprCompare e1 e2
else (if morePrecise m1 m2 then Lt else Gt)
| Downcast _ _, Binop _ _ _ => Lt
| Downcast _ _, _ => Gt
......@@ -55,16 +55,16 @@ val expCompare_def = Define `
in
(case res of
| Eq =>
(case expCompare e11 e21 of
| Eq => expCompare e12 e22
(case exprCompare e11 e21 of
| Eq => exprCompare e12 e22
| Lt => Lt
| Gt => Gt)
| _ => res)
| Fma e1 e2 e3, Fma e4 e5 e6 =>
(case expCompare e1 e4 of
(case exprCompare e1 e4 of
| Eq =>
(case expCompare e2 e5 of
| Eq => expCompare e3 e6
(case exprCompare e2 e5 of
| Eq => exprCompare e3 e6
| Lt => Lt
| Gt => Gt)
| Lt => Lt
......@@ -73,23 +73,23 @@ val expCompare_def = Define `
| Fma e1 e2 e3, _ => Gt
|_ , _ => Gt`;
val expCompare_refl = store_thm (
"expCompare_refl",
``!e. expCompare e e = Eq``,
Induct \\ rpt strip_tac \\ simp[ Once expCompare_def]
val exprCompare_refl = store_thm (
"exprCompare_refl",
``!e. exprCompare e e = Eq``,
Induct \\ rpt strip_tac \\ simp[ Once exprCompare_def]
\\ Cases_on `b` \\ fs[] );
val FloverMapList_insert_def = Define `
(FloverMapList_insert e k NIL = [(e,k)]) /\
(FloverMapList_insert e k ((e1,l1) :: el) =
case expCompare e e1 of
case exprCompare e e1 of
| Lt => (e,k)::(e1,l1)::el
| Eq => (e1,l1) :: el
| Gt => (e1,l1):: FloverMapList_insert e k el)`;
val FloverMapList_find_def = Define `
(FloverMapList_find e NIL = NONE) /\
(FloverMapList_find e ((e1,k)::el) = if expCompare e e1 = Eq then SOME k else FloverMapList_find e el)`;
(FloverMapList_find e ((e1,k)::el) = if exprCompare e e1 = Eq then SOME k else FloverMapList_find e el)`;
val _ = Datatype `
binTree = Node 'a binTree binTree | Leaf 'a | LeafN`;
......@@ -97,12 +97,12 @@ val _ = Datatype `
val FloverMapTree_insert_def = Define `
(FloverMapTree_insert e k LeafN = Leaf (e,k)) /\
(FloverMapTree_insert e k (Leaf (e1,k1)) =
case (expCompare e e1) of
case (exprCompare e e1) of
| Lt => Node (e1,k1) (Leaf (e,k)) (LeafN)
| Eq => Leaf (e1,k)
| Gt => Node (e1,k1) (LeafN) (Leaf (e,k))) /\
(FloverMapTree_insert e k (Node (e1,k1) tl tr) =
case (expCompare e e1) of
case (exprCompare e e1) of
| Lt => Node (e1,k1) (FloverMapTree_insert e k tl) tr
| Eq => (Node (e1, k) tl tr)
| Gt => Node (e1,k1) tl (FloverMapTree_insert e k tr))`;
......@@ -110,9 +110,9 @@ val FloverMapTree_insert_def = Define `
val FloverMapTree_find_def = Define `
(FloverMapTree_find e (LeafN) = NONE) /\
(FloverMapTree_find e (Leaf (e1,k1)) =
if expCompare e e1 = Eq then SOME k1 else NONE) /\
if exprCompare e e1 = Eq then SOME k1 else NONE) /\
(FloverMapTree_find e (Node (e1,k1) tl tr) =
case (expCompare e e1) of
case (exprCompare e e1) of
| Lt => FloverMapTree_find e tl
| Eq => SOME k1
| Gt => FloverMapTree_find e tr)`;
......@@ -141,14 +141,11 @@ val FloverMapTree_correct = store_thm (
FloverMapTree_find k (FloverMapTree_insert k v Tree) = SOME v``,
Induct_on `Tree`
\\ fs[FloverMapTree_find_def, FloverMapTree_insert_def]
\\ rpt strip_tac \\ fs[expCompare_refl]
\\ rpt strip_tac \\ fs[exprCompare_refl]
>- (Cases_on `a` \\ fs[FloverMapTree_insert_def]
\\ Cases_on `expCompare k q` \\ fs[FloverMapTree_find_def]
\\ Cases_on `exprCompare k q` \\ fs[FloverMapTree_find_def]
\\ first_x_assum irule \\ fs[])
\\ Cases_on `a` \\ fs[FloverMapTree_insert_def]
\\ Cases_on `expCompare k q` \\ fs[FloverMapTree_find_def, expCompare_refl]);
val _ = type_abbrev ("typeMap", ``:(real exp # mType) binTree``);
val _ = type_abbrev ("analysisResult", ``:(real exp # ((real # real) # real)) binTree``);
\\ Cases_on `exprCompare k q` \\ fs[FloverMapTree_find_def, exprCompare_refl]);
val _ = export_theory();
This diff is collapsed.
......@@ -16,6 +16,10 @@ val _ = Datatype `
mType = REAL | M16 | M32 | M64(* | M128 | M256 *)
|F num num (*first num is word length, second is fractional bits *)`;
val isFixedPoint_def = Define `
isFixedPoint (F w f) = T /\
isFixedPoint _ = F`;
val mTypeToR_def = Define `
mTypeToR (m:mType) : real =
case m of
......@@ -46,7 +50,9 @@ val computeError_up = store_thm (
``!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
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)`
......@@ -66,14 +72,14 @@ val isMorePrecise_def = Define `
isMorePrecise (m1:mType) (m2:mType) =
case m1, m2 of
| REAL, _ => T
| F w1 f1, F w2 f2 => w1 <= w2
| F w1 f1, F w2 f2 => w2 <= w1
| F w f, _ => F
| _, F w f => F
| _, _ => (mTypeToR (m1) <= mTypeToR (m2))`;
val morePrecise_def = Define `
(morePrecise REAL _ = T) /\
(morePrecise (F w1 f1) (F w2 f2) = (w1 <= w2)) /\
(morePrecise (F w1 f1) (F w2 f2) = (w2 <= w1)) /\
(morePrecise (F w f) _ = F) /\
(morePrecise _ (F w f) = F) /\
(morePrecise M16 M16 = T) /\
......@@ -110,6 +116,11 @@ val isMorePrecise_morePrecise = store_thm (
\\ once_rewrite_tac [morePrecise_def, isMorePrecise_def]
\\ fs[morePrecise_def, isMorePrecise_def, mTypeToR_def]);
val isMorePrecise_refl = store_thm (
"isMorePrecise_refl",
``!m. isMorePrecise m m``,
Cases_on `m` \\ EVAL_TAC \\ fs[]);
val REAL_least_precision = store_thm ("REAL_least_precision",
``!(m:mType).
isMorePrecise m REAL ==>
......@@ -130,27 +141,37 @@ val REAL_lower_bound = store_thm ("REAL_lower_bound",
has to happen in 64 bits
**)
val join_def = Define `
join (m1:mType) (m2:mType) =
if (morePrecise m1 m2) then m1 else m2`;
join (F w1 f1) (F w2 f2) (fBit:num) =
SOME (F (if w1 <= w2 then w2 else w1) fBit) /\
join (F w f) _ _ = NONE /\
join _ (F w f) _ = NONE /\
join (m1:mType) (m2:mType) (fBit:num) =
if (morePrecise m1 m2) then SOME m1 else SOME m2`;
val join_float = store_thm (
"join_float",
``!m1 m2 f1 f2.
isFixedPoint m1 = F /\
isFixedPoint m2 = F ==>
join m1 m2 f1 = join m1 m2 f2``,
rpt strip_tac \\ Cases_on `m1` \\ Cases_on `m2`
\\ fs[join_def, isFixedPoint_def] );
val join3_def = Define `
join3 (m1: mType) (m2: mType) (m3: mType) = join m1 (join m2 m3)`;
(* val REAL_join_is_REAL = store_thm ("REAL_join_is_REAL", *)
(* ``!m1 m2. *)
(* join m1 m2 = REAL ==> *)
(* (m1 = REAL /\ m2 = REAL)``, *)
(* fs [join_def, isMorePrecise_def] *)
(* \\ rpt strip_tac *)
(* \\ 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 [mTypeToR_def]) *)
(* >- (Cases_on `m2` \\ fs [mTypeToR_def])); *)
join3 (m1: mType) (m2: mType) (m3: mType) (fBit:num) =
case (join m2 m3) fBit of
| SOME m => join m1 m fBit
| NONE => NONE`
val join3_float = store_thm (
"join3_float",
``!m1 m2 m3 f1 f2.
isFixedPoint m1 = F /\
isFixedPoint m2 = F /\
isFixedPoint m3 = F ==>
join3 m1 m2 m3 f1 = join3 m1 m2 m3 f2``,
rpt strip_tac \\ Cases_on `m1` \\ Cases_on `m2` \\ Cases_on `m3`
\\ fs[join3_def, join_def, isFixedPoint_def, morePrecise_def]);
val maxExponent_def = Define `
(maxExponent (REAL) = 0n) /\
......@@ -180,7 +201,7 @@ which simplifies to 2^(e_max) for base 2
val maxValue_def = Define `
maxValue (m:mType) =
case m of
| F w f => &((2n ** (w-1)) - 1) * &(2n ** (maxExponent m))
| F w f => &((2n ** (w-1)) - 1) * inv &(2n ** (maxExponent m))
| _ => (&(2n ** (maxExponent m))):real`;
(** Using the sign bit, the very same number is representable as a negative number,
......@@ -195,10 +216,6 @@ val minValue_pos_def = Define `
(** 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 - 1))`;
val normal_def = Define `
normal (v:real) (m:mType) =
(minValue_pos m <= abs v /\ abs v <= maxValue m)`;
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -32,21 +32,21 @@ val check_rec_def = Define `
case num_fun of
| SUC n' =>
(case dParse input of
| SOME ((dCmd, P, A, Gamma),NIL) =>
if CertificateCheckerCmd dCmd A P Gamma
| SOME ((dCmd, P, A, Gamma, fBits),NIL) =>
if CertificateCheckerCmd dCmd A P Gamma fBits
then "True\n"
else "False\n"
| SOME ((dCmd, P, A, Gamma), residual) =>
if CertificateCheckerCmd dCmd A P Gamma
| SOME ((dCmd, P, A, Gamma, fBits), residual) =>
if CertificateCheckerCmd dCmd A P Gamma fBits
then check_rec residual n'
else "False\n"
| NONE => pp input(*"parse failure\n"*))
| _ => "failure num of functions"`;
val check_def = Define `
check (f:real cmd) (P:precond) (A:analysisResult) Gamma (n:num) =
check (f:real cmd) (P:precond) (A:analysisResult) Gamma fBits (n:num) =
case n of
| SUC n' => (CertificateCheckerCmd f A P Gamma /\ check f P A Gamma n')
| SUC n' => (CertificateCheckerCmd f A P Gamma fBits /\ check f P A Gamma fBits n')
| _ => T`
val check_all_def = Define `
......@@ -54,8 +54,8 @@ val check_all_def = Define `
case num_fun of
| SUC n =>
(case (dParse input) of
| SOME ((f,P,A, Gamma), residual) =>
if (check f P A Gamma iters)
| SOME ((f,P,A, Gamma, fBits), residual) =>
if (check f P A Gamma fBits iters)
then case residual of
| a:: b => check_all n iters residual
| NIL => "True\n"
......@@ -188,7 +188,7 @@ val maxValue_eq = prove(
| M16 => maxValueM16
| M32 => maxValueM32
| M64 => maxValueM64
| F w f => &(2 ** (w 1) 1) * &(2 ** maxExponent m)``,
| F w f => &(2 ** (w 1) 1) * inv &(2 ** maxExponent m)``,
Cases_on `m` \\ EVAL_TAC)
|> translate;
......@@ -294,13 +294,13 @@ val precond_validIntervalboundsCmd_true = prove (
\\ fs []));
val precond_validErrorbound_true = prove (``
!P f expTypes A (dVars:num_set).
!P f exprTypes A (dVars:num_set).
(!v. v IN (domain dVars) ==>
?iv err.
FloverMapTree_find (Var v) A = SOME (iv, err) /\
valid iv) /\
validIntervalbounds f A P dVars ==>
validerrorbound_side f expTypes A dVars ``,
validerrorbound_side f exprTypes A dVars ``,
gen_tac
\\ recInduct validErrorbound_ind
\\ rpt gen_tac
......@@ -374,13 +374,13 @@ val precond_validErrorbound_true = prove (``
\\ first_x_assum irule \\ fs[]);
val precond_errorbounds_true = prove (``
!P f expTypes A dVars.
!P f exprTypes A dVars.
(!v. v IN (domain dVars) ==>
?iv err.
FloverMapTree_find (Var v) A = SOME (iv, err) /\
valid iv) /\
validIntervalboundsCmd f A P dVars ==>
validerrorboundcmd_side f expTypes A dVars``,
validerrorboundcmd_side f exprTypes A dVars``,
gen_tac
\\ recInduct validErrorboundCmd_ind
\\ rpt strip_tac
......@@ -402,8 +402,8 @@ val precond_errorbounds_true = prove (``
\\ qexists_tac `P` \\ fs []);