Commit 316f0b15 authored by Heiko Becker's avatar Heiko Becker

Port CC functions

parent 58bb46dc
......@@ -4,10 +4,11 @@
validator and the error bound validator. Running this function on the encoded
analysis result gives the desired theorem as shown in the soundness theorem.
**)
open simpLib realTheory realLib RealArith RealSimpsTheory
open simpLib realTheory realLib RealArith RealSimpsTheory;
open AbbrevsTheory ExpressionsTheory FloverTactics ExpressionAbbrevsTheory
ErrorBoundsTheory IntervalArithTheory IntervalValidationTheory
ErrorValidationTheory ssaPrgsTheory FPRangeValidatorTheory
ExpressionSemanticsTheory ErrorBoundsTheory IntervalArithTheory
RealRangeArithTheory IntervalValidationTheory ErrorValidationTheory
ssaPrgsTheory FPRangeValidatorTheory TypeValidatorTheory FloverMapTheory;
open preamble;
......@@ -17,14 +18,15 @@ val _ = temp_overload_on("abs",``real$abs``);
(** Certificate checking function **)
val CertificateChecker_def = Define
`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)
else F
else F`;
(defVars: typeMap)=
case getValidMap defVars e FloverMapTree_empty of
| Fail s => F
| FailDet _ _ => F
| Succes Gamma =>
if (validIntervalbounds e A P LN /\
FPRangeValidator e A Gamma LN)
then (validErrorbound e Gamma A LN)
else F`;
(**
Soundness proof for the certificate checker.
......@@ -32,22 +34,22 @@ val CertificateChecker_def = Define
the real valued execution respects the precondition.
**)
val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
``!(e:real expr) (A:analysisResult) (P:precond) (E1 E2:env) defVars fVars fBits.
approxEnv E1 defVars A fVars LN E2 /\
``!(e:real expr) (A:analysisResult) (P:precond) (E1 E2:env) defVars fVars.
(!v.
v IN (domain fVars) ==>
?vR.
(E1 v = SOME vR) /\
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 fBits ==>
CertificateChecker e A P defVars ==>
? Gamma.
approxEnv E1 (toRExpMap Gamma) A fVars LN E2 ==>
?iv err vR vF m.
FloverMapTree_find e A = SOME (iv,err) /\
eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval e) vR REAL /\
eval_expr E2 defVars (toRBMap fBits) e vF m /\
eval_expr E1 (toRTMap (toRExpMap Gamma)) (toREval e) vR REAL /\
eval_expr E2 (toRExpMap Gamma) e vF m /\
(!vF m.
eval_expr E2 defVars (toRBMap fBits) e vF m ==>
eval_expr E2 (toRExpMap Gamma) e vF m ==>
abs (vR - vF) <= err /\ validFloatValue vF m)``,
(**
The proofs is a simple composition of the soundness proofs for the range
......@@ -55,73 +57,88 @@ val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
**)
simp [CertificateChecker_def]
\\ rpt strip_tac
\\ Cases_on `getValidMap defVars e FloverMapTree_empty` \\ fs[]
\\ IMP_RES_TAC getValidMap_top_correct
\\ `validTypes e a`
by (first_x_assum irule
\\ fs[FloverMapTree_empty_def, FloverMapTree_mem_def, FloverMapTree_find_def])
\\ drule validIntervalbounds_sound
\\ rpt (disch_then drule)
\\ disch_then (qspecl_then [`fVars`,`E1`, `defVars`, `toRBMap fBits`] destruct)
\\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]
\\ disch_then (qspecl_then [`fVars`,`E1`, `a`] destruct)
\\ fs[dVars_range_valid_def, fVars_P_sound_def]
\\ qexists_tac `a` \\ rpt strip_tac
\\ drule validErrorbound_sound
\\ rpt (disch_then drule)
\\ disch_then (qspecl_then [`vR`, `err`, `P`, `FST iv`, `SND iv`] destruct)
\\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]
\\ rpt (asm_exists_tac \\ fs[])
\\ IMP_RES_TAC validRanges_single
\\ disch_then (qspecl_then [`vR`, `err`, `FST iv`, `SND iv`] destruct)
\\ fs[]
\\ rpt (find_exists_tac \\ fs[])
\\ rpt strip_tac
>- (first_x_assum irule \\ fs[]
\\ asm_exists_tac \\ fs[])
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ disch_then irule
\\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]);
\\ disch_then irule \\ fs[]);
val CertificateCheckerCmd_def = Define
`CertificateCheckerCmd (f:real cmd) (absenv:analysisResult) (P:precond)
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) /\
FPRangeValidatorCmd f absenv tMap LN)
then (validErrorboundCmd f tMap absenv LN)
else F
else F`;
defVars =
case getValidMapCmd defVars f FloverMapTree_empty of
| Fail _ => F
| FailDet _ _ => F
| Succes tMap =>
if (validSSA f (freeVars f))
then
if ((validIntervalboundsCmd f absenv P LN) /\
FPRangeValidatorCmd f absenv tMap LN)
then (validErrorboundCmd f tMap absenv LN)
else F
else F`;
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) fBits.
approxEnv E1 defVars A (freeVars f) LN E2 /\
(E1 E2:env) (fVars:num_set).
(!v.
v IN (domain (freeVars f)) ==>
?vR.
(E1 v = SOME vR) /\
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 fBits ==>
?iv err vR vF m.
FloverMapTree_find (getRetExp f) A = SOME (iv, 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)``,
CertificateCheckerCmd f A P defVars ==>
? Gamma.
approxEnv E1 (toRExpMap Gamma) A (freeVars f) LN E2 ==>
?iv err vR vF m.
FloverMapTree_find (getRetExp f) A = SOME (iv, err) /\
bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
bstep f E2 (toRExpMap Gamma) vF m /\
(!vF m. bstep f E2 (toRExpMap Gamma) vF m ==> abs (vR - vF) <= err)``,
simp [CertificateCheckerCmd_def]
\\ rpt strip_tac
\\ Cases_on `getValidMapCmd defVars f FloverMapTree_empty` \\ fs[]
\\ IMP_RES_TAC getValidMapCmd_correct
\\ `validTypesCmd f a`
by (first_x_assum irule
\\ fs[FloverMapTree_empty_def, FloverMapTree_mem_def, FloverMapTree_find_def])
\\ qexists_tac `a` \\ 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`, `toRBMap fBits`]
[`f`, `A`, `E1`, `freeVars f`, `LN`, `outVars`, `P`, `a`]
destruct validIntervalboundsCmd_sound
\\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]
\\ fs[dVars_range_valid_def, fVars_P_sound_def]
\\ IMP_RES_TAC validRangesCmd_single
\\ qspecl_then
[`f`, `A`, `E1`, `E2`, `outVars`, `freeVars f`, `LN`, `vR`, `FST iv`,
`SND iv`, `err`, `P`, `m`, `typeMapCmd defVars f FloverMapTree_empty fBits`,
`defVars`, `fBits`]
[`f`, `A`, `E1`, `E2`, `outVars`, `freeVars f`, `LN`, `vR`, `FST iv_e`,
`SND iv_e`, `err_e`, `m`, `a`]
destruct validErrorboundCmd_gives_eval
\\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]
\\ rpt (asm_exists_tac \\ fs[])
\\ fs[]
\\ rpt (find_exists_tac \\ fs[])
\\ rpt strip_tac
\\ drule validErrorboundCmd_sound
\\ rpt (disch_then drule)
\\ 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]);
\\ rename1 `bstep f E2 _ vF2 m2`
\\ disch_then
(qspecl_then
[`outVars`, `vR`, `vF2`, `FST iv_e`, `SND iv_e`, `err_e`, `m2`] destruct)
\\ fs[]);
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