Commit a28258ab authored by Heiko Becker's avatar Heiko Becker

Next step of finite map port

parent 730713b3
(**
This file contains the HOL4 implementation of the certificate checker as well as its soundness proof.
The checker is a composition of the range analysis validator and the error bound validator.
Running this function on the encoded analysis result gives the desired theorem
as shown in the soundness theorem.
This file contains the HOL4 implementation of the certificate checker as well
as its soundness proof. The checker is a composition of the range analysis
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 preamble
open preamble;
open simpLib realTheory realLib RealArith RealSimpsTheory
open AbbrevsTheory ExpressionsTheory DaisyTactics ExpressionAbbrevsTheory
......@@ -16,29 +16,24 @@ val _ = temp_overload_on("abs",``real$abs``);
(** Certificate checking function **)
val CertificateChecker_def = Define
`CertificateChecker (e:real exp) (absenv:analysisResult) (P:precond) (defVars: num -> mType option)=
if (typeCheck e defVars (typeMap defVars e)) then
if (validIntervalbounds e absenv P LN /\ FPRangeValidator e absenv (typeMap defVars e) LN) then
(validErrorbound e (typeMap defVars e) absenv LN)
`CertificateChecker (e:real exp) (A:analysisResult) (P:precond)
(defVars: num -> mType option) =
let tMap = typeMap defVars e DaisyMapTree_empty in
if (typeCheck e defVars tMap) then
if (validIntervalbounds e A P LN /\
FPRangeValidator e A tMap LN)
then (validErrorbound e tMap A LN)
else F
else F`;
val CertificateCheckerCmd_def = Define
`CertificateCheckerCmd (f:real cmd) (absenv:analysisResult) (P:precond) defVars =
if (typeCheckCmd f defVars (typeMapCmd defVars f) /\ validSSA f (freeVars f)) then
if ((validIntervalboundsCmd f absenv P LN) /\ FPRangeValidatorCmd f absenv (typeMapCmd defVars f) LN) then
(validErrorboundCmd f (typeMapCmd defVars f) absenv LN)
else F
else F`;
(**
Soundness proof for the certificate checker.
Apart from assuming two executions, one in R and one on floats, we assume that
the real valued execution respects the precondition.
**)
val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
``!(e:real exp) (absenv:analysisResult) (P:precond) (E1 E2:env) defVars fVars.
approxEnv E1 defVars absenv fVars LN E2 /\
``!(e:real exp) (A:analysisResult) (P:precond) (E1 E2:env) defVars fVars.
approxEnv E1 defVars A fVars LN E2 /\
(!v.
v IN (domain fVars) ==>
?vR.
......@@ -46,44 +41,54 @@ 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 absenv P defVars ==>
?vR vF m.
CertificateChecker e A P defVars ==>
?iv err vR vF m.
DaisyMapTree_find e A = SOME (iv,err) /\
eval_exp E1 (toRMap defVars) (toREval e) vR M0 /\
eval_exp E2 defVars e vF m /\
(!vF m.
eval_exp E2 defVars e vF m ==>
abs (vR - vF) <= (SND (absenv e)) /\ validFloatValue vF m)``,
abs (vR - vF) <= err /\ validFloatValue vF m)``,
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
simp [CertificateChecker_def]
\\ rpt strip_tac
\\ Cases_on `absenv e`
\\ rename1 `absenv e = (iv, err)`
\\ Cases_on `iv`
\\ rename1 `absenv e = ((elo, ehi), err)`
\\ qspecl_then
[`e`, `absenv` , `P` , `fVars`, `LN`, `E1`, `defVars`]
destruct validIntervalbounds_sound
\\ fs[]
\\ qspecl_then
[`e`, `E1`, `E2`, `absenv`, `vR`, `err`, `P`, `elo`, `ehi`, `fVars`,
`LN`, `typeMap defVars e`, `defVars`]
destruct validErrorbound_sound
\\ fs[]
\\ qexistsl_tac [`vR`, `nF`, `m`] \\ fs[]
\\ drule validIntervalbounds_sound
\\ rpt (disch_then drule)
\\ disch_then (qspecl_then [`fVars`,`E1`, `defVars`] destruct)
\\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]
\\ 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[])
\\ rpt strip_tac
>- (first_x_assum irule \\ fs[]
\\ asm_exists_tac \\ fs[])
\\ irule FPRangeValidator_sound
\\ qexistsl_tac [`absenv`, `E1`, `E2`, `defVars`, `P`, `LN`,`e`, `fVars`, `typeMap defVars e`]
\\ fs[]);
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ disch_then irule
\\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]);
val CertificateCheckerCmd_def = Define
`CertificateCheckerCmd (f:real cmd) (absenv:analysisResult) (P:precond)
defVars =
let tMap = typeMapCmd defVars f DaisyMapTree_empty in
if (typeCheckCmd f defVars tMap /\
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) (absenv:analysisResult) (P:precond) defVars
``!(f:real cmd) (A:analysisResult) (P:precond) defVars
(E1 E2:env) (fVars:num_set).
approxEnv E1 defVars absenv (freeVars f) LN E2 /\
approxEnv E1 defVars A (freeVars f) LN E2 /\
(!v.
v IN (domain (freeVars f)) ==>
?vR.
......@@ -91,31 +96,32 @@ 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 absenv P defVars ==>
?vR vF m.
CertificateCheckerCmd f A P defVars ==>
?iv err vR vF m.
DaisyMapTree_find (getRetExp f) A = SOME (iv, err) /\
bstep (toREvalCmd f) E1 (toRMap defVars) vR M0 /\
bstep f E2 defVars vF m /\
(!vF m. bstep f E2 defVars vF m ==> abs (vR - vF) <= (SND (absenv (getRetExp f))))``,
(!vF m. bstep f E2 defVars 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[])
\\ Cases_on `absenv (getRetExp f)`
\\ rename1 `absenv (getRetExp f) = (iv, err)`
\\ Cases_on `iv`
\\ rename1 `absenv (getRetExp f) = ((elo, ehi), err)`
\\ qspecl_then
[`f`, `absenv`, `E1`, `freeVars f`, `LN`, `outVars`, `elo`, `ehi`, `err`, `P`, `defVars`]
[`f`, `A`, `E1`, `freeVars f`, `LN`, `outVars`, `elo`, `ehi`, `err`, `P`, `defVars`]
destruct validIntervalboundsCmd_sound
\\ fs[]
\\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]
\\ qspecl_then
[`f`, `absenv`, `E1`, `E2`, `outVars`, `freeVars f`, `LN`, `vR`, `elo`, `ehi`, `err`, `P`, `m`, `typeMapCmd defVars f`, `defVars`]
[`f`, `A`, `E1`, `E2`, `outVars`, `freeVars f`, `LN`, `vR`, `FST iv`,
`SND iv`, `err`, `P`, `m`, `typeMapCmd defVars f DaisyMapTree_empty`,
`defVars`]
destruct validErrorboundCmd_gives_eval
\\ fs[]
\\ qexistsl_tac [`vR`, `vF`, `m`] \\ fs[]
\\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]
\\ rpt (asm_exists_tac \\ fs[])
\\ rpt strip_tac
\\ irule validErrorboundCmd_sound
\\ drule validErrorboundCmd_sound
\\ rpt (disch_then drule)
\\ rename1 `bstep f E2 defVars vF2 m2`
\\ qexistsl_tac [`E1`, `E2`, `defVars`, `P`, `absenv`, `LN`, `ehi`, `elo`,`typeMapCmd defVars f`, `f`, `freeVars f`, `m2`, `outVars`]
\\ fs[]);
\\ 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]);
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