Commit 65bfd34f authored by Heiko Becker's avatar Heiko Becker
Browse files

Change return type of checker for integration with CakeML

parent 23cf55c1
......@@ -16,33 +16,36 @@ val _ = new_theory "CertificateChecker";
val _ = temp_overload_on("abs",``real$abs``);
(** Certificate checking function **)
val CertificateChecker_def = Define
`CertificateChecker (e:real expr) (A:analysisResult) (P:precond)
Definition CertificateChecker_def:
CertificateChecker (e:real expr) (A:analysisResult) (P:precond)
(defVars: typeMap)=
case getValidMap defVars e FloverMapTree_empty of
| Fail s => F
| FailDet _ _ => F
(case getValidMap defVars e FloverMapTree_empty of
| Fail s => NONE
| FailDet _ _ => NONE
| Succes Gamma =>
if (validIntervalbounds e A P LN /\
FPRangeValidator e A Gamma LN)
then (validErrorbound e Gamma A LN)
else F`;
then
if validErrorbound e Gamma A LN
then SOME Gamma
else NONE
else NONE)
End
(**
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 expr) (A:analysisResult) (P:precond) (E1 E2:env) defVars fVars.
Theorem Certificate_checking_is_sound:
!(e:real expr) (A:analysisResult) (P:precond) (E1 E2:env) defVars fVars Gamma.
(!v.
v IN (domain fVars) ==>
?vR.
(E1 v = SOME vR) /\
FST (P v) <= vR /\ vR <= SND (P v)) /\
(domain (usedVars e)) SUBSET (domain fVars) /\
CertificateChecker e A P defVars ==>
? Gamma.
CertificateChecker e A P defVars = SOME Gamma /\
approxEnv E1 (toRExpMap Gamma) A fVars LN E2 ==>
?iv err vR vF m.
FloverMapTree_find e A = SOME (iv,err) /\
......@@ -50,7 +53,8 @@ val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
eval_expr E2 (toRExpMap Gamma) e vF m /\
(!vF m.
eval_expr E2 (toRExpMap Gamma) e vF m ==>
abs (vR - vF) <= err /\ validFloatValue vF m)``,
abs (vR - vF) <= err /\ validFloatValue vF m)
Proof
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
......@@ -59,14 +63,14 @@ val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
\\ rpt strip_tac
\\ Cases_on `getValidMap defVars e FloverMapTree_empty` \\ fs[]
\\ IMP_RES_TAC getValidMap_top_correct
\\ `validTypes e a`
\\ rveq
\\ `validTypes e Gamma`
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`, `a`] destruct)
\\ disch_then (qspecl_then [`fVars`,`E1`, `Gamma`] destruct)
\\ fs[dVars_range_valid_def, fVars_P_sound_def]
\\ qexists_tac `a` \\ rpt strip_tac
\\ drule validErrorbound_sound
\\ rpt (disch_then drule)
\\ IMP_RES_TAC validRanges_single
......@@ -78,57 +82,61 @@ val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
\\ asm_exists_tac \\ fs[])
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ disch_then irule \\ fs[]);
\\ disch_then irule \\ fs[]
QED
val CertificateCheckerCmd_def = Define
`CertificateCheckerCmd (f:real cmd) (absenv:analysisResult) (P:precond)
Definition CertificateCheckerCmd_def:
CertificateCheckerCmd (f:real cmd) (absenv:analysisResult) (P:precond)
defVars =
case getValidMapCmd defVars f FloverMapTree_empty of
| Fail _ => F
| FailDet _ _ => F
| Succes tMap =>
(case getValidMapCmd defVars f FloverMapTree_empty of
| Fail _ => NONE
| FailDet _ _ => NONE
| Succes Gamma =>
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`;
FPRangeValidatorCmd f absenv Gamma LN)
then
if validErrorboundCmd f Gamma absenv LN
then SOME Gamma
else NONE
else NONE
else NONE)
End
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).
Theorem CertificateCmd_checking_is_sound:
!(f:real cmd) (A:analysisResult) (P:precond) defVars
(E1 E2:env) (fVars:num_set) Gamma.
(!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) /\
CertificateCheckerCmd f A P defVars ==>
? Gamma.
approxEnv E1 (toRExpMap Gamma) A (freeVars f) LN E2 ==>
CertificateCheckerCmd f A P defVars = SOME 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)``,
(!vF m. bstep f E2 (toRExpMap Gamma) vF m ==> abs (vR - vF) <= err)
Proof
simp [CertificateCheckerCmd_def]
\\ rpt strip_tac
\\ Cases_on `getValidMapCmd defVars f FloverMapTree_empty` \\ fs[]
\\ IMP_RES_TAC getValidMapCmd_correct
\\ `validTypesCmd f a`
\\ rveq \\ imp_res_tac getValidMapCmd_correct
\\ `validTypesCmd f Gamma`
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`, `a`]
[`f`, `A`, `E1`, `freeVars f`, `LN`, `outVars`, `P`, `Gamma`]
destruct validIntervalboundsCmd_sound
\\ 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_e`,
`SND iv_e`, `err_e`, `m`, `a`]
`SND iv_e`, `err_e`, `m`, `Gamma`]
destruct validErrorboundCmd_gives_eval
\\ fs[]
\\ rpt (find_exists_tac \\ fs[])
......@@ -139,6 +147,7 @@ val CertificateCmd_checking_is_sound = store_thm ("CertificateCmd_checking_is_so
\\ disch_then
(qspecl_then
[`outVars`, `vR`, `vF2`, `FST iv_e`, `SND iv_e`, `err_e`, `m2`] destruct)
\\ fs[]);
\\ fs[]
QED
val _ = export_theory();
open simpLib realTheory realLib RealArith sptreeTheory;
open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory
FloverTactics FloverMapTheory;
FloverTactics FloverMapTheory MachineTypeTheory;
open preambleFloVer;
val _ = new_theory "Environments";
val _ = temp_overload_on("abs",``real$abs``);
val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
(!(Gamma: real expr -> mType option) (A:analysisResult).
approxEnv emptyEnv Gamma A LN LN emptyEnv) /\
(!(E1:env) (E2:env) (Gamma: real expr -> mType option) (A:analysisResult)
Definition approxEnv_def:
approxEnv E1 Gamma absEnv (fVars:num_set) (dVars:num_set) E2 =
((* No variable defined twice *)
domain fVars INTER domain dVars = EMPTY
(* environments are only defined for the domain *)
( x. ~ (x IN (domain fVars UNION domain dVars))
E1 x = NONE E2 x = NONE)
(* All free variables are bounded in error by their machine epsilon *)
( x. x IN domain fVars
m v1 v2.
Gamma (Var x) = SOME m
E1 x = SOME v1
E2 x = SOME v2
abs (v1 - v2) computeError v1 m)
(* All bound variables are bounded in error by their inferred bound *)
( x. x IN domain dVars
m iv err v1 v2.
Gamma (Var x) = SOME m
E1 x = SOME v1
E2 x = SOME v2
FloverMapTree_find (Var x) absEnv = SOME (iv, err)
abs (v1 - v2) err))
End
Theorem approxEnvRefl:
approxEnv emptyEnv Gamma A LN LN emptyEnv
Proof
simp[approxEnv_def]
QED
Theorem approxEnvUpdFree:
(!(E1:env) (E2:env) (Gamma: real expr -> mType option) (A:analysisResult)
(fVars:num_set) (dVars:num_set) v1 v2 x.
approxEnv E1 Gamma A fVars dVars E2 /\
(Gamma (Var x) = SOME m) /\
......@@ -18,8 +46,29 @@ val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1)
Gamma A (insert x () fVars) dVars
(updEnv x v2 E2)) /\
(!(E1:env) (E2:env) (Gamma: real expr -> mType option) (A:analysisResult)
(updEnv x v2 E2))
Proof
rw[] \\ fs[approxEnv_def] \\ rpt conj_tac
>- (
fs[EXTENSION, lookup_union, option_case_eq]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ metis_tac[domain_lookup])
>- (
rpt strip_tac \\ rveq \\ res_tac
\\ fsrw_tac [SATISFY_ss] []
\\ x' x
by (CCONTR_TAC \\ fs[] \\ rveq
\\ fs[lookup_union, option_case_eq, domain_lookup])
\\ fs[])
\\ rpt strip_tac \\ res_tac \\ fsrw_tac [SATISFY_ss] []
\\ x' x
by (CCONTR_TAC \\ fs[] \\ rveq
\\ fs[lookup_union, option_case_eq, domain_lookup])
\\ fs[]
QED
Theorem approxEnvUpdBound:
(E1:env) (E2:env) (Gamma: real expr -> mType option) (A:analysisResult)
(fVars:num_set) (dVars:num_set) v1 v2 x iv err.
approxEnv E1 Gamma A fVars dVars E2 /\
Gamma (Var x) = SOME m /\
......@@ -28,100 +77,82 @@ val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1)
Gamma A fVars (insert x () dVars)
(updEnv x v2 E2))`;
(updEnv x v2 E2)
Proof
rw[] \\ fs[approxEnv_def] \\ rpt conj_tac
>- (
fs[EXTENSION, lookup_union, option_case_eq]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ metis_tac[domain_lookup])
>- (
rpt strip_tac \\ rveq \\ res_tac
\\ fsrw_tac [SATISFY_ss] []
\\ x' x
by (CCONTR_TAC \\ fs[] \\ rveq
\\ fs[lookup_union, option_case_eq, domain_lookup])
\\ fs[])
\\ rpt strip_tac \\ res_tac \\ fsrw_tac [SATISFY_ss] []
\\ x' x
by (CCONTR_TAC \\ fs[] \\ rveq
\\ fs[lookup_union, option_case_eq, domain_lookup])
\\ fs[]
QED
val [approxRefl, approxUpdFree, approxUpdBound] = CONJ_LIST 3 approxEnv_rules;
save_thm ("approxRefl", approxRefl);
save_thm ("approxUpdFree", approxUpdFree);
save_thm ("approxUpdBound", approxUpdBound);
val approxEnv_rules = LIST_CONJ [approxEnvRefl, approxEnvUpdFree, approxEnvUpdBound]
val _ = save_thm ("approxEnv_rules", approxEnv_rules);
val approxEnv_gives_value = store_thm (
"approxEnv_gives_value",
``!E1 E2 x v (fVars:num_set) (dVars:num_set) absenv Gamma.
approxEnv E1 Gamma absenv fVars dVars E2 /\
E1 x = SOME v /\
x IN ((domain fVars) UNION (domain dVars)) ==>
?v2.
E2 x = SOME v2``,
qspec_then
`\E1 Gamma absenv fVars dVars E2.
!x v.
E1 x = SOME v /\
x IN ((domain fVars) UNION (domain dVars)) ==>
?v2. E2 x = SOME v2` (fn thm => assume_tac (SIMP_RULE std_ss [] thm)) approxEnv_ind
\\ rpt strip_tac \\ first_x_assum irule
\\ rpt strip_tac
>- (fs [domain_union, updEnv_def, lookup_union] \\ rveq
\\ EVERY_CASE_TAC \\ fs[])
>- (fs [domain_union, updEnv_def, lookup_union] \\ rveq
\\ EVERY_CASE_TAC \\ fs[])
>- (qexistsl_tac [`E1`, `Gamma`, `absenv`, `fVars`, `dVars`] \\ fs []));
Theorem approxEnv_gives_value:
!E1 E2 x v (fVars:num_set) (dVars:num_set) absenv Gamma.
approxEnv E1 Gamma absenv fVars dVars E2 /\
E1 x = SOME v /\
x IN ((domain fVars) UNION (domain dVars)) ==>
?v2. E2 x = SOME v2
Proof
rw[approxEnv_def] \\ res_tac \\ fsrw_tac [SATISFY_ss] []
QED
val approxEnv_fVar_bounded = store_thm (
"approxEnv_fVar_bounded",
``!E1 Gamma absenv fVars dVars E2 x v v2 m.
Theorem approxEnv_fVar_bounded:
!E1 Gamma absenv fVars dVars E2 x v v2 m.
approxEnv E1 Gamma absenv fVars dVars E2 /\
E1 x = SOME v /\
E2 x = SOME v2 /\
x IN (domain fVars) /\
Gamma (Var x) = SOME m ==>
abs (v - v2) <= computeError v m``,
rpt strip_tac
\\ qspec_then
`\E1 Gamma absenv fVars dVars E2.
!x v v2 m.
E1 x = SOME v /\
E2 x = SOME v2 /\
x IN (domain fVars) /\
Gamma (Var x) = SOME m ==>
abs (v - v2) <= computeError v m`
(fn thm => irule (SIMP_RULE std_ss [] thm))
approxEnv_ind
\\ rpt strip_tac
>- (fs [])
>- (fs []
\\ EVERY_CASE_TAC \\ rveq \\ fs[lookup_union, domain_lookup]
\\ first_x_assum drule \\ fs[])
>- (fs []
\\ rveq \\ fs[]
\\ EVERY_CASE_TAC
\\ rveq \\ fs[]
\\ first_x_assum drule \\ fs[])
\\ qexistsl_tac [`E1`, `Gamma`, `absenv`, `fVars`, `dVars`, `E2`, `x`]
\\ fs[]);
abs (v - v2) <= computeError v m
Proof
rw[approxEnv_def] \\ res_tac \\ fs[]
\\ metis_tac[]
QED
val approxEnv_dVar_bounded = store_thm ("approxEnv_dVar_bounded",
``!E1 Gamma A fVars dVars E2 x v v2 m iv e.
Theorem approxEnv_dVar_bounded:
!E1 Gamma A fVars dVars E2 x v v2 m iv e.
approxEnv E1 Gamma A fVars dVars E2 /\
E1 x = SOME v /\
E2 x = SOME v2 /\
x IN (domain dVars) /\
Gamma (Var x) = SOME m /\
FloverMapTree_find (Var x) A = SOME (iv, e) ==>
abs (v - v2) <= e``,
rpt strip_tac
\\ qspec_then
`\E1 Gamma A fVars dVars E2.
!x v v2 m.
E1 x = SOME v /\
E2 x = SOME v2 /\
x IN (domain dVars) /\
Gamma (Var x) = SOME m /\
FloverMapTree_find (Var x) A = SOME (iv, e) ==>
abs (v - v2) <= e`
(fn thm => destruct (SIMP_RULE std_ss [] thm))
approxEnv_ind
>- (rpt conj_tac
>- (fs [emptyEnv_def])
>- (rpt strip_tac \\ fs [updEnv_def]
\\ EVERY_CASE_TAC \\ rveq \\ fs[lookup_union, domain_lookup]
>- (EVERY_CASE_TAC \\ fs[])
\\ first_x_assum drule \\ fs[])
>- (rpt strip_tac \\ fs [updEnv_def, updDefVars_def] \\ rveq \\ fs[]
\\ EVERY_CASE_TAC \\ rveq \\ fs[]
\\ first_x_assum drule \\ fs[]))
\\ first_x_assum drule
\\ rpt (disch_then drule)
\\ disch_then MATCH_ACCEPT_TAC);
abs (v - v2) <= e
Proof
rw[approxEnv_def] \\ res_tac \\ fs[]
\\ metis_tac[]
QED
Theorem approxEnv_refl:
fVars dVars E1 Gamma A.
(domain fVars INTER domain dVars = EMPTY)
( x. x IN (domain fVars) UNION (domain dVars)
v. E1 x = SOME v)
( x. ~ (x IN (domain fVars) UNION (domain dVars))
E1 x = NONE)
( x. x IN (domain dVars) err iv. FloverMapTree_find (Var x) A = SOME (iv, err) 0 err)
( x. x IN (domain fVars) UNION (domain dVars)
m. Gamma (Var x) = SOME m)
approxEnv E1 Gamma A fVars dVars E1
Proof
rw[approxEnv_def] \\ res_tac \\ fsrw_tac [SATISFY_ss] []
\\ Cases_on m \\ fs[computeError_def, mTypeToR_pos]
\\ irule REAL_LE_MUL \\ fs[mTypeToR_pos]
QED
val _ = export_theory ();;
......@@ -17,7 +17,7 @@ open preambleFloVer;
val _ = new_theory "ErrorIntervalInference";
val inferErrorbound_def = Define `
Definition inferErrorbound_def:
inferErrorbound e (typeMap: typeMap) (I:ivMap) (akk:analysisResult) :analysisResult option=
(case (FloverMapTree_find e akk) of
| SOME _ => SOME akk
......@@ -103,9 +103,10 @@ val inferErrorbound_def = Define `
in
SOME (FloverMapTree_insert e (iv_f, eNew) recRes)
od)
od)`;
od)
End
val inferErrorboundCmd_def = Define `
Definition inferErrorboundCmd_def:
inferErrorboundCmd (f:real cmd) (typeMap: (real expr # mType) binTree)
(I:ivMap) (akk:analysisResult) =
case f of
......@@ -116,6 +117,7 @@ val inferErrorboundCmd_def = Define `
inferErrorboundCmd g typeMap I (FloverMapTree_insert (Var x) (ive, erre) recRes);
od
| Ret e =>
inferErrorbound e typeMap I akk`;
inferErrorbound e typeMap I akk
End
val _ = export_theory();
......@@ -2581,7 +2581,7 @@ val validErrorboundCmd_gives_eval = store_thm (
\\ rename1 `eval_expr E2 (toRExpMap Gamma) e vF mF`
\\ `approxEnv (updEnv n v E1) (toRExpMap Gamma) A fVars
(insert n () dVars) (updEnv n vF E2)`
by (irule approxUpdBound \\ fs[lookup_NONE_domain]
by (irule approxEnvUpdBound \\ fs[lookup_NONE_domain]
\\ conj_tac
>- (qexists_tac `m` \\ fs[toRExpMap_def])
\\ first_x_assum irule \\ find_exists_tac \\ fs[])
......@@ -2666,7 +2666,7 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound",
\\ once_rewrite_tac [UNION_COMM]
\\ fs [INSERT_UNION_EQ])
>- (fs[Once toREvalCmd_def])
>- (irule approxUpdBound \\ rpt conj_tac
>- (irule approxEnvUpdBound \\ rpt conj_tac
\\ fs[]
>- (fs[Once validTypesCmd_def] \\ fs[toRExpMap_def])
>- (Cases_on `lookup n (union fVars dVars)` \\ fs [domain_lookup])
......
......@@ -223,7 +223,7 @@ val FPRangeValidatorCmd_sound = store_thm (
`fVars`, `insert n () dVars`, `outVars`]
impl_subgoal_tac)
>- (fs[] \\ rpt conj_tac
>- (irule approxUpdBound \\ fs[lookup_NONE_domain]
>- (irule approxEnvUpdBound \\ fs[lookup_NONE_domain]
\\ conj_tac
>- (fs[Once validTypesCmd_def, toRExpMap_def])
\\ first_x_assum (qspecl_then [`vF`, `m`] irule)
......
......@@ -1148,7 +1148,7 @@ val bstep_gives_IEEE = store_thm (
impl_subgoal_tac
validErrorboundCmd_gives_eval
>- (fs[] \\ rpt conj_tac
>- (irule approxUpdBound
>- (irule approxEnvUpdBound
\\ fs[lookup_NONE_domain, toRExpMap_def])
>- (irule ssa_equal_set
\\ qexists_tac `insert n () (union fVars dVars)`
......@@ -1190,7 +1190,7 @@ val bstep_gives_IEEE = store_thm (
\\ rpt conj_tac
>- (strip_tac \\ fs[updFlEnv_def, updEnv_def, toREnv_def]
\\ IF_CASES_TAC \\ fs[])
>- (drule approxUpdBound
>- (drule approxEnvUpdBound
\\ disch_then
(qspecl_then
[`M64`, `v'`, `float_to_real (fp64_to_float v_e)`, `n`]
......@@ -1426,16 +1426,15 @@ val getValidMapCmd_preserving = store_thm (
val IEEE_connection_expr = store_thm (
"IEEE_connection_expr",
``!(e:word64 expr) (A:analysisResult) (P:precond) E1 E2 defVars fVars.
``!(e:word64 expr) (A:analysisResult) (P:precond) E1 E2 defVars fVars Gamma.
is64BitEval (toRExp e) /\
is64BitEnv defVars /\
noDowncast (toRExp e) /\
eval_expr_valid e E2 /\
fVars_P_sound fVars E1 P /\
(domain (usedVars (toRExp e))) SUBSET (domain fVars) /\
CertificateChecker (toRExp e) A P defVars ==>
? Gamma.
approxEnv E1 (toRExpMap Gamma) A fVars LN (toREnv E2) ==>
CertificateChecker (toRExp e) A P defVars = SOME Gamma /\
approxEnv E1 (toRExpMap Gamma) A fVars LN (toREnv E2) ==>
?iv err vR vF. (* m, currently = M64 *)
FloverMapTree_find (toRExp e) A = SOME (iv, err) /\
eval_expr E1 (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) vR REAL /\
......@@ -1446,31 +1445,30 @@ val IEEE_connection_expr = store_thm (
simp [CertificateChecker_def]
\\ rpt strip_tac
\\ Cases_on `getValidMap defVars (toRExp e) FloverMapTree_empty` \\ fs[]
\\ IMP_RES_TAC getValidMap_top_correct
\\ `validTypes (toRExp e) a`
\\ rveq \\ IMP_RES_TAC getValidMap_top_correct
\\ `validTypes (toRExp e) Gamma`
by (first_x_assum irule
\\ fs[FloverMapTree_empty_def, FloverMapTree_mem_def, FloverMapTree_find_def])
\\ `! e m. FloverMapTree_find e a = SOME m ==> m = M64`
\\ `! e m. FloverMapTree_find e Gamma = SOME m ==> m = M64`
by (rpt strip_tac \\ irule getValidMap_preserving
\\ qexistsl_tac [`FloverMapTree_empty`, `defVars`, `toRExp e`, `e'`, `a`]
\\ qexistsl_tac [`FloverMapTree_empty`, `defVars`, `toRExp e`, `e'`, `Gamma`]
\\ rpt conj_tac \\ rpt strip_tac
\\ fs[FloverMapTree_empty_def, FloverMapTree_find_def , is64BitEnv_def]
\\ first_x_assum irule \\ find_exists_tac \\ fs[])
\\ qexists_tac `a` \\ rpt strip_tac
\\ drule validIntervalbounds_sound
\\ rpt (disch_then drule)
\\ disch_then (qspecl_then [`fVars`,`E1`, `a`] destruct)
\\ disch_then (qspecl_then [`fVars`,`E1`, `Gamma`] destruct)
\\ fs[dVars_range_valid_def, fVars_P_sound_def]
\\ drule validErrorbound_sound
\\ rpt (disch_then drule)
\\ IMP_RES_TAC validRanges_single
\\ disch_then (qspecl_then [`vR`, `err`, `FST iv`, `SND iv`] destruct)
\\ fs[]
\\ qspecl_then [`e`, `E1`, `E2`, `toREnv E2`, `a`, `nF`, `A`, `fVars`, `LN`]
\\ qspecl_then [`e`, `E1`, `E2`, `toREnv E2`, `Gamma`, `nF`, `A`, `fVars`, `LN`]
destruct
eval_expr_gives_IEEE
>- (rpt conj_tac \\ fs[]
>- (`FloverMapTree_find (toRExp e) a = SOME M64`
>- (`FloverMapTree_find (toRExp e) Gamma = SOME M64`
by (irule typing_expr_64bit \\ fs[is64BitEnv_def]
\\ first_x_assum MATCH_ACCEPT_TAC)
\\ `m = M64`
......@@ -1482,16 +1480,16 @@ val IEEE_connection_expr = store_thm (
val IEEE_connection_cmds = store_thm (
"IEEE_connection_cmds",
``! (f:word64 cmd) (A:analysisResult) (P:precond) E1 E2 defVars (fVars:num_set).
``! (f:word64 cmd) (A:analysisResult) (P:precond) E1 E2 defVars (fVars:num_set)
Gamma.
is64BitBstep (toRCmd f) /\
is64BitEnv defVars /\
noDowncastFun (toRCmd f) /\
bstep_valid f E2 /\
fVars_P_sound fVars E1 P /\
(domain (freeVars (toRCmd f))) SUBSET (domain fVars) /\
CertificateCheckerCmd (toRCmd f) A P defVars ==>
? Gamma.
approxEnv E1 (toRExpMap Gamma) A (freeVars (toRCmd f)) LN (toREnv E2) ==>
CertificateCheckerCmd (toRCmd f) A P defVars = SOME Gamma /\
approxEnv E1 (toRExpMap Gamma) A (freeVars (toRCmd f)) LN (toREnv E2) ==>
?iv err vR vF. (* m, currently = M64 *)
FloverMapTree_find (getRetExp (toRCmd f)) A = SOME (iv, err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
......@@ -1502,38 +1500,37 @@ val IEEE_connection_cmds = store_thm (
simp [CertificateCheckerCmd_def]
\\ rpt strip_tac
\\ Cases_on `getValidMapCmd defVars (toRCmd f) FloverMapTree_empty` \\ fs[]
\\ IMP_RES_TAC getValidMapCmd_correct
\\ `validTypesCmd (toRCmd f) a`
\\ rveq \\ IMP_RES_TAC getValidMapCmd_correct
\\ `validTypesCmd (toRCmd f) Gamma`
by (first_x_assum irule
\\ fs[FloverMapTree_empty_def, FloverMapTree_mem_def, FloverMapTree_find_def])
\\ `! e m. FloverMapTree_find e a = SOME m ==> m = M64`
\\ `! e m. FloverMapTree_find e Gamma = SOME m ==> m = M64`
by (rpt strip_tac \\ irule getValidMapCmd_preserving
\\ qexistsl_tac [`FloverMapTree_empty`, `defVars`, `e`, `toRCmd f`, `a`]
\\ qexistsl_tac [`FloverMapTree_empty`, `defVars`, `e`, `toRCmd f`, `Gamma`]
\\ rpt conj_tac \\ rpt strip_tac
\\ fs[FloverMapTree_empty_def, FloverMapTree_find_def , is64BitEnv_def]
\\ first_x_assum irule \\ find_exists_tac \\ fs[])
\\ qexists_tac `a`