diff --git a/hol4/CertificateCheckerScript.sml b/hol4/CertificateCheckerScript.sml
index bcad1f2ddc179e1a1ff831ecfbfedc715e3f01f5..70de241dfad14e1911b19057c2db43560ea5315c 100644
--- a/hol4/CertificateCheckerScript.sml
+++ b/hol4/CertificateCheckerScript.sml
@@ -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();
diff --git a/hol4/EnvironmentsScript.sml b/hol4/EnvironmentsScript.sml
index 7fefb0d861f6262a409135a03018a2c06807dfd2..86b25426e8f38ca546cec277b0dbd82fc6c5ba5d 100644
--- a/hol4/EnvironmentsScript.sml
+++ b/hol4/EnvironmentsScript.sml
@@ -1,16 +1,44 @@
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 ();;
diff --git a/hol4/ErrorIntervalInferenceScript.sml b/hol4/ErrorIntervalInferenceScript.sml
index 7b51d3ed882aa2b98768284376c8bf606fd02d8a..69821ef040e8c1a182b53364ba09658c73672bb1 100644
--- a/hol4/ErrorIntervalInferenceScript.sml
+++ b/hol4/ErrorIntervalInferenceScript.sml
@@ -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();
diff --git a/hol4/ErrorValidationScript.sml b/hol4/ErrorValidationScript.sml
index 668d7c6b62882631325fb62f58623719e5cd703f..c0ba05f0c94f7d01c61ee2f8b4fe567a95b20c6f 100644
--- a/hol4/ErrorValidationScript.sml
+++ b/hol4/ErrorValidationScript.sml
@@ -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])
diff --git a/hol4/FPRangeValidatorScript.sml b/hol4/FPRangeValidatorScript.sml
index 2daa757c01d396cbcaa7918f3a56cd60f9255fd6..6a0614c11a4eb05cbbb8f1f7eb145038f697b9c5 100644
--- a/hol4/FPRangeValidatorScript.sml
+++ b/hol4/FPRangeValidatorScript.sml
@@ -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)
diff --git a/hol4/IEEE_connectionScript.sml b/hol4/IEEE_connectionScript.sml
index c0d6851e244f990780b60208eb7723180d6c6da7..7bca265d85cb154021172e8d093371c8807c42be 100644
--- a/hol4/IEEE_connectionScript.sml
+++ b/hol4/IEEE_connectionScript.sml
@@ -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` \\ rpt strip_tac
\\ `?outVars. ssa (toRCmd f) (freeVars (toRCmd f)) outVars`
by (match_mp_tac validSSA_sound \\ fs[])
\\ qspecl_then
- [`toRCmd f`, `A`, `E1`, `freeVars (toRCmd f)`, `LN`, `outVars`, `P`, `a`]
+ [`toRCmd f`, `A`, `E1`, `freeVars (toRCmd f)`, `LN`, `outVars`, `P`, `Gamma`]
destruct validIntervalboundsCmd_sound
\\ fs[dVars_range_valid_def, fVars_P_sound_def]
>- (rpt strip_tac \\ first_x_assum irule \\ fs[SUBSET_DEF])
\\ IMP_RES_TAC validRangesCmd_single
\\ qspecl_then
[`toRCmd f`, `A`, `E1`, `toREnv E2`, `outVars`, `freeVars (toRCmd f)`, `LN`, `vR`, `FST iv_e`,
- `SND iv_e`, `err_e`, `M64`, `a`]
+ `SND iv_e`, `err_e`, `M64`, `Gamma`]
destruct validErrorboundCmd_gives_eval
\\ fs[]
\\ rpt (find_exists_tac \\ fs[])
\\ qspecl_then
- [`f`, `E1`, `E2`, `toREnv E2`, `a`, `vR`, `vF`, `A`, `freeVars (toRCmd f)`, `LN`, `outVars`]
+ [`f`, `E1`, `E2`, `toREnv E2`, `Gamma`, `vR`, `vF`, `A`, `freeVars (toRCmd f)`, `LN`, `outVars`]
destruct
bstep_gives_IEEE
>- (fs[is64BitEnv_def]
\\ conj_tac
- >- (`FloverMapTree_find (getRetExp (toRCmd f)) a = SOME M64`
+ >- (`FloverMapTree_find (getRetExp (toRCmd f)) Gamma = SOME M64`
by (irule typing_cmd_64bit
\\ fs[is64BitEnv_def] \\ first_x_assum MATCH_ACCEPT_TAC)
\\ `m = M64`
@@ -1541,7 +1538,7 @@ val IEEE_connection_cmds = store_thm (
\\ disch_then assume_tac \\ fs[]
\\ fs[] \\ rveq \\ fs[]
\\ first_x_assum irule
- \\ qexistsl_tac [`toREnv E2`, `a`, `vF`] \\ fs[])
+ \\ qexistsl_tac [`toREnv E2`, `Gamma`, `vF`] \\ fs[])
\\ rveq \\ fs[])
\\ first_x_assum MATCH_ACCEPT_TAC)
\\ find_exists_tac \\ fs[]
diff --git a/hol4/RealIntervalInferenceScript.sml b/hol4/RealIntervalInferenceScript.sml
index 0389b8a33edee365c771a4109fd0ec4b0a0b8f1d..ab9d3520a904031023f7c34d9dadbd86080a58a7 100644
--- a/hol4/RealIntervalInferenceScript.sml
+++ b/hol4/RealIntervalInferenceScript.sml
@@ -1,12 +1,8 @@
(**
- Interval arithmetic checker and its soundness proof.
- The function validIntervalbounds checks wether the given analysis result is
- a valid range arithmetic for each sub term of the given exprression e.
- The computation is done using our formalized interval arithmetic.
- The function is used in CertificateChecker.v to build the full checker.
+ Implement a trusted, unverified inferencer for real range intervals.
+ The inferred, returned maps should be run through the certificate checker
**)
-open simpLib realTheory realLib RealArith pred_setTheory sptreeTheory
- sptreeLib;
+open simpLib realTheory realLib RealArith;
open AbbrevsTheory ExpressionsTheory RealSimpsTheory FloverTactics
ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory
MachineTypeTheory FloverMapTheory TypeValidatorTheory RealRangeArithTheory
@@ -19,61 +15,63 @@ val _ = monadsyntax.enable_monadsyntax();
val _ = List.app monadsyntax.enable_monad ["option"];
val _ = type_abbrev ("ivMap", ``:(real # real) fMap``);
-val inferIntervalbounds_def = Define `
- inferIntervalbounds f (P:precond) (akk:ivMap) :ivMap option =
- (case (FloverMapTree_find f akk) of
+(** Unverified, trusted inferencer for interval bounds on expressions **)
+Definition inferIntervalbounds_def:
+ inferIntervalbounds e (P:precond) (akk:ivMap) :ivMap option =
+ (case (FloverMapTree_find e akk) of
| SOME intv => SOME akk
| NONE =>
- (case f of
- | Var v =>
- SOME (FloverMapTree_insert f (P v) akk)
- | Const m n =>
- SOME (FloverMapTree_insert f (n,n) akk)
- | Unop op f1 =>
+ (case e of
+ | Var v =>
+ SOME (FloverMapTree_insert e (P v) akk)
+ | Const m n =>
+ SOME (FloverMapTree_insert e (n,n) akk)
+ | Unop op e1 =>
do
- recRes <- inferIntervalbounds f1 P akk;
- iv_f1 <- FloverMapTree_find f1 recRes;
+ recRes <- inferIntervalbounds e1 P akk;
+ iv_e1 <- FloverMapTree_find e1 recRes;
case op of
| Neg =>
- SOME (FloverMapTree_insert f (negateInterval iv_f1) recRes)
+ SOME (FloverMapTree_insert e (negateInterval iv_e1) recRes)
| _ => NONE
od
- | Downcast m f1 =>
+ | Downcast m e1 =>
do
- recRes <- inferIntervalbounds f1 P akk;
- iv_f1 <- FloverMapTree_find f1 recRes;
- SOME (FloverMapTree_insert f iv_f1 recRes);
+ recRes <- inferIntervalbounds e1 P akk;
+ iv_e1 <- FloverMapTree_find e1 recRes;
+ SOME (FloverMapTree_insert e iv_e1 recRes);
od
- | Binop op f1 f2 =>
+ | Binop op e1 e2 =>
do
- recRes1 <- inferIntervalbounds f1 P akk;
- recRes2 <- inferIntervalbounds f2 P recRes1;
- iv_f1 <- FloverMapTree_find f1 recRes2;
- iv_f2 <- FloverMapTree_find f2 recRes2;
- if (op = Div /\ (IVlo iv_f2 <= 0 /\ 0 <= IVhi iv_f2))
+ recRes1 <- inferIntervalbounds e1 P akk;
+ recRes2 <- inferIntervalbounds e2 P recRes1;
+ iv_e1 <- FloverMapTree_find e1 recRes2;
+ iv_e2 <- FloverMapTree_find e2 recRes2;
+ if (op = Div /\ (IVlo iv_e2 <= 0 /\ 0 <= IVhi iv_e2))
then NONE
else
SOME
(let new_iv =
(case op of
- | Plus => addInterval iv_f1 iv_f2
- | Sub => subtractInterval iv_f1 iv_f2
- | Mult => multInterval iv_f1 iv_f2
- | Div => divideInterval iv_f1 iv_f2)
- in FloverMapTree_insert f new_iv recRes2);
+ | Plus => addInterval iv_e1 iv_e2
+ | Sub => subtractInterval iv_e1 iv_e2
+ | Mult => multInterval iv_e1 iv_e2
+ | Div => divideInterval iv_e1 iv_e2)
+ in FloverMapTree_insert e new_iv recRes2);
od
- | Fma f1 f2 f3 =>
+ | Fma e1 e2 e3 =>
do
- recRes1 <- inferIntervalbounds f1 P akk;
- recRes2 <- inferIntervalbounds f2 P recRes1;
- recRes3 <- inferIntervalbounds f3 P recRes2;
- iv_f1 <- FloverMapTree_find f1 recRes3;
- iv_f2 <- FloverMapTree_find f2 recRes3;
- iv_f3 <- FloverMapTree_find f3 recRes3;
- SOME (FloverMapTree_insert f (addInterval iv_f1 (multInterval iv_f2 iv_f3)) recRes3);
- od))`;
+ recRes1 <- inferIntervalbounds e1 P akk;
+ recRes2 <- inferIntervalbounds e2 P recRes1;
+ recRes3 <- inferIntervalbounds e3 P recRes2;
+ iv_e1 <- FloverMapTree_find e1 recRes3;
+ iv_e2 <- FloverMapTree_find e2 recRes3;
+ iv_e3 <- FloverMapTree_find e3 recRes3;
+ SOME (FloverMapTree_insert e (addInterval iv_e1 (multInterval iv_e2 iv_e3)) recRes3);
+ od))
+End
-val inferIntervalboundsCmd_def = Define `
+Definition inferIntervalboundsCmd_def:
inferIntervalboundsCmd (f:real cmd) (P:precond) (akk:ivMap) :ivMap option =
case f of
| Let m x e g =>
@@ -82,6 +80,7 @@ val inferIntervalboundsCmd_def = Define `
iv_x <- FloverMapTree_find e recRes;
inferIntervalboundsCmd g P (FloverMapTree_insert (Var x) iv_x recRes);
od
- | Ret e => inferIntervalbounds e P akk`;
+ | Ret e => inferIntervalbounds e P akk
+End
val _ = export_theory();
diff --git a/testcases/regression/certificate_AdditionSimpleScript.sml b/testcases/regression/certificate_AdditionSimpleScript.sml
index 5e0d64ff4e2971726b6840e29798dea91755f11e..4152d5475afb9205bf95c0626ca55611b70d0012 100644
--- a/testcases/regression/certificate_AdditionSimpleScript.sml
+++ b/testcases/regression/certificate_AdditionSimpleScript.sml
@@ -24,8 +24,9 @@ val absenv_additionSimple_def = RIGHT_CONV_RULE EVAL (Define `
FloverMapTree_insert PlusC12u0 (( (1157)/(5), (2157)/(5)), (7771411516990528329)/(81129638414606681695789005144064)) (FloverMapTree_insert u0 (( (-100)/(1), (100)/(1)), (25)/(2251799813685248)) (FloverMapTree_insert C12 (( (1657)/(5), (1657)/(5)), (1657)/(45035996273704960)) (FloverMapTree_empty)))`);
val _ = store_thm ("ErrorBound_additionSimple_Sound",
-``CertificateCheckerCmd RetPlusC12u0 absenv_additionSimple thePreconditionadditionSimple defVars_additionSimple``,
+``? Gamma. CertificateCheckerCmd RetPlusC12u0 absenv_additionSimple
+thePreconditionadditionSimple defVars_additionSimple = SOME Gamma``,
flover_eval_tac \\ fs[REAL_INV_1OVER]);
- val _ = export_theory();
\ No newline at end of file
+ val _ = export_theory();
diff --git a/testcases/regression/certificate_DopplerScript.sml b/testcases/regression/certificate_DopplerScript.sml
index 27f2e7b02520442a73a31164d05d1d8f1a4d5a26..88ef069ea29c50377635121aac489ee659dbb908 100644
--- a/testcases/regression/certificate_DopplerScript.sml
+++ b/testcases/regression/certificate_DopplerScript.sml
@@ -36,8 +36,10 @@ val absenv_doppler_def = RIGHT_CONV_RULE EVAL (Define `
FloverMapTree_insert (Var 5) (( (1567)/(5), (1807)/(5)) , (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert DivMultUMint15v1MultPlust15u0Plust15u0 (( (-180700000)/(1138489), (-156700)/(5322249)), (3128798615377558964734587413815260935766775940003133188505004688351541231456980597512692494850911181122476079460422247077079176104347591604229243224768895229048954292495195716430601972291603510900358841802949847973326821449585470105361794370971246392326730165769086503662250520953800794720080442853388469377023727444437325832874114769965213547362197536886857310450874114551302656316164631446184855133337791662127325138346785397490340980930573694307935576641198224172023812349312175410753884375)/(32036808664321353711103483032138488273658359037549607658529725639211828966830820254532621633000657987120666498279218129796043154742555162761269493533793888535784577584907972014998498622632370186488026019213317308445273559994196553084922725810710211676061848042954653773443813684285036579995330627524678538042961243278389567362111169788921619483881120057899533645621131479344403647093086239019570741449266701692934633407390503406115529744843066088021266694728367150101865392734271463782370359902208)) (FloverMapTree_insert MultPlust15u0Plust15u0 (( (1138489)/(25), (5322249)/(25)), (221418104607549167303687710004535513986647169788185712517024989429754271464351432210081914542156799340890022745270932056774650467829092329282443134010319379819395881176728139368810835608677)/(11138771039116687545510672865479226867415108660274804518015606733152527263693060025649201199505301268990825951107408220973361095511170502925421536425103061983037096372949865600788267070914560)) (FloverMapTree_insert Plust15u0 (( (1067)/(5), (2307)/(5)), (53564494515561689875478770421278470058449227170380936038373717166064943312314302539)/(2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280)) (FloverMapTree_insert u0 (( (-100)/(1), (100)/(1)), (25)/(2251799813685248)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert Plust15u0 (( (1067)/(5), (2307)/(5)), (53564494515561689875478770421278470058449227170380936038373717166064943312314302539)/(2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280)) (FloverMapTree_insert u0 (( (-100)/(1), (100)/(1)), (25)/(2251799813685248)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert MultUMint15v1 (( (-7228000)/(1), (-6268)/(1)), (627708954014028785690670388543358359225843737736535036700014937775757601384955913375)/(485667223056432267729865476705879726660601709763034880312953102434726071301302124544)) (FloverMapTree_insert v1 (( (20)/(1), (20000)/(1)), (625)/(524288)) (FloverMapTree_insert UMint15 (( (-1807)/(5), (-1567)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert CastM32PlusC12MultC34T2 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert PlusC12MultC34T2 (( (1567)/(5), (1807)/(5)), (286015870425657721837309664377505636991869898457103)/(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMapTree_insert MultC34T2 (( (-18)/(1), (30)/(1)), (3650833728657301081634471694827535)/(365375409332725729550921208179070754913983135744)) (FloverMapTree_insert T2 (( (-30)/(1), (50)/(1)), (25)/(4503599627370496)) (FloverMapTree_insert C34 (( (3)/(5), (3)/(5)), (3)/(45035996273704960)) (FloverMapTree_insert C12 (( (1657)/(5), (1657)/(5)), (1657)/(45035996273704960)) (FloverMapTree_empty)))))))))))))))))))`);
val _ = store_thm ("ErrorBound_doppler_Sound",
-``CertificateCheckerCmd Lett15CastM32PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0 absenv_doppler thePreconditiondoppler defVars_doppler``,
+``?Gamma. CertificateCheckerCmd
+Lett15CastM32PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0
+absenv_doppler thePreconditiondoppler defVars_doppler = SOME Gamma``,
flover_eval_tac \\ fs[REAL_INV_1OVER]);
- val _ = export_theory();
\ No newline at end of file
+ val _ = export_theory();
diff --git a/testcases/regression/certificate_HimmilbeauScript.sml b/testcases/regression/certificate_HimmilbeauScript.sml
index 1f0054035219170b93b6abc730cfff5bbddd05b6..b9e169cbced20dfb4ac9ec03a977a06c2e84f863 100644
--- a/testcases/regression/certificate_HimmilbeauScript.sml
+++ b/testcases/regression/certificate_HimmilbeauScript.sml
@@ -39,8 +39,10 @@ val absenv_himmilbeau_def = RIGHT_CONV_RULE EVAL (Define `
FloverMapTree_insert (Var 4) (( (-30)/(1), (30)/(1)) , (1961594369037173916351814399292228280199748452939370332185)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert (Var 5) (( (-30)/(1), (30)/(1)) , (4466206448905498720458189731062635560985)/(713623846352979940529142984724747568191373312)) (FloverMapTree_insert PlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 (( (-1630)/(1), (3050)/(1)), (139030704224875129848631128264048621058694569279811803247481731950009496854900927199310534682209129985511707022154285854387010824157493138914819710540399882149220846561084929737220738253425)/(285152538601387201165073225356268207805826781703034995661199532368704697950542336656619550707335712486165144348349650456918044045085964874890791332482638386765749667147516559380179637015412736)) (FloverMapTree_insert MultSubt25C34Subt25C34 (( (-851)/(1), (1369)/(1)), (172349177736374561212483578428963824900652162571585970864206741278453079284487093344235995612234246229019482224189617435933207648273009)/(372141426839350727961253789638658321589064376671906846864122981980487315514059736743009817965446945567110411062408283101969716033850703872)) (FloverMapTree_insert Subt25C34 (( (-37)/(1), (23)/(1)), (40228011429500474146133911235065735963306515172659036185)/(6427752177035961102167848369364650410088811975131171341205504)) (FloverMapTree_insert C34 (( (7)/(1), (7)/(1)), (7)/(9007199254740992)) (FloverMapTree_insert t25 (( (-30)/(1), (30)/(1)), (4466206448905498720458189731062635560985)/(713623846352979940529142984724747568191373312)) (FloverMapTree_insert Subt25C34 (( (-37)/(1), (23)/(1)), (40228011429500474146133911235065735963306515172659036185)/(6427752177035961102167848369364650410088811975131171341205504)) (FloverMapTree_insert C34 (( (7)/(1), (7)/(1)), (7)/(9007199254740992)) (FloverMapTree_insert t25 (( (-30)/(1), (30)/(1)), (4466206448905498720458189731062635560985)/(713623846352979940529142984724747568191373312)) (FloverMapTree_insert MultSubt14C12Subt14C12 (( (-779)/(1), (1681)/(1)), (773662351057808216309562571440580964132485471675311443368294135882643818858939959011276491221639706451414523198800188781950039677633553108167639838248029929043321394561649)/(31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408)) (FloverMapTree_insert Subt14C12 (( (-41)/(1), (19)/(1)), (17668471681160709216739148477143291992482578503008842760016586714686423065)/(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMapTree_insert C12 (( (11)/(1), (11)/(1)), (11)/(9007199254740992)) (FloverMapTree_insert t14 (( (-30)/(1), (30)/(1)), (1961594369037173916351814399292228280199748452939370332185)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert Subt14C12 (( (-41)/(1), (19)/(1)), (17668471681160709216739148477143291992482578503008842760016586714686423065)/(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMapTree_insert C12 (( (11)/(1), (11)/(1)), (11)/(9007199254740992)) (FloverMapTree_insert t14 (( (-30)/(1), (30)/(1)), (1961594369037173916351814399292228280199748452939370332185)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert CastM32Plusx10Multx21x21 (( (-30)/(1), (30)/(1)), (4466206448905498720458189731062635560985)/(713623846352979940529142984724747568191373312)) (FloverMapTree_insert Plusx10Multx21x21 (( (-30)/(1), (30)/(1)), (190147601533197042302697458892825)/(42535295865117307932921825928971026432)) (FloverMapTree_insert Multx21x21 (( (-25)/(1), (25)/(1)), (21110624511590425)/(4722366482869645213696)) (FloverMapTree_insert x21 (( (-5)/(1), (5)/(1)), (5)/(16777216)) (FloverMapTree_insert x21 (( (-5)/(1), (5)/(1)), (5)/(16777216)) (FloverMapTree_insert x10 (( (-5)/(1), (5)/(1)), (5)/(9007199254740992)) (FloverMapTree_insert PlusMultx10x10x21 (( (-30)/(1), (30)/(1)), (1961594369037173916351814399292228280199748452939370332185)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert x21 (( (-5)/(1), (5)/(1)), (5)/(16777216)) (FloverMapTree_insert Multx10x10 (( (-25)/(1), (25)/(1)), (6084722881095501802724119491379225)/(730750818665451459101842416358141509827966271488)) (FloverMapTree_insert x10 (( (-5)/(1), (5)/(1)), (5)/(9007199254740992)) (FloverMapTree_insert x10 (( (-5)/(1), (5)/(1)), (5)/(9007199254740992)) (FloverMapTree_empty))))))))))))))))))))))))))))`);
val _ = store_thm ("ErrorBound_himmilbeau_Sound",
-``CertificateCheckerCmd Lett14PlusMultx10x10x21Lett25CastM32Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 absenv_himmilbeau thePreconditionhimmilbeau defVars_himmilbeau``,
+``? Gamma. CertificateCheckerCmd
+Lett14PlusMultx10x10x21Lett25CastM32Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34
+absenv_himmilbeau thePreconditionhimmilbeau defVars_himmilbeau = SOME Gamma``,
flover_eval_tac \\ fs[REAL_INV_1OVER]);
- val _ = export_theory();
\ No newline at end of file
+ val _ = export_theory();