Skip to content

Commit 432d81b

Browse files
HeikoBeckerHeikoBecker
committed
Integrate FloVer with the RealCake work
1 parent b75bf3c commit 432d81b

37 files changed

+12896
-0
lines changed

‎icing/flover/.HOLCOMMIT

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
cf32220437a948e43d98b65374ff189830d0baf2

‎icing/flover/CertificateCheckerScript.sml

+161
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,161 @@
1+
(**
2+
This file contains the HOL4 implementation of the certificate checker as well
3+
as its soundness proof. The checker is a composition of the range analysis
4+
validator and the error bound validator. Running this function on the encoded
5+
analysis result gives the desired theorem as shown in the soundness theorem.
6+
**)
7+
open simpLib realTheory realLib RealArith RealSimpsTheory;
8+
open AbbrevsTheory ExpressionsTheory FloverTactics ExpressionAbbrevsTheory
9+
ExpressionSemanticsTheory ErrorBoundsTheory IntervalArithTheory
10+
RealRangeArithTheory IntervalValidationTheory ErrorValidationTheory
11+
ssaPrgsTheory FPRangeValidatorTheory TypeValidatorTheory FloverMapTheory;
12+
13+
open preambleFloVer;
14+
15+
val _ = new_theory "CertificateChecker";
16+
val _ = temp_overload_on("abs",``real$abs``);
17+
18+
(** Certificate checking function **)
19+
Definition CertificateChecker_def:
20+
CertificateChecker (e:real expr) (A:analysisResult) (P:precond)
21+
(defVars: typeMap)=
22+
(case getValidMap defVars e FloverMapTree_empty of
23+
| Fail s => NONE
24+
| FailDet _ _ => NONE
25+
| Succes Gamma =>
26+
if (validIntervalbounds e A P LN /\
27+
FPRangeValidator e A Gamma LN)
28+
then
29+
if validErrorbound e Gamma A LN
30+
then SOME Gamma
31+
else NONE
32+
else NONE)
33+
End
34+
35+
(**
36+
Soundness proof for the certificate checker.
37+
Apart from assuming two executions, one in R and one on floats, we assume that
38+
the real valued execution respects the precondition.
39+
**)
40+
Theorem Certificate_checking_is_sound:
41+
!(e:real expr) (A:analysisResult) (P:precond) (E1 E2:env) defVars fVars Gamma.
42+
(!v.
43+
v IN (domain fVars) ==>
44+
?vR.
45+
(E1 v = SOME vR) /\
46+
FST (P v) <= vR /\ vR <= SND (P v)) /\
47+
(domain (usedVars e)) SUBSET (domain fVars) /\
48+
CertificateChecker e A P defVars = SOME Gamma /\
49+
approxEnv E1 (toRExpMap Gamma) A fVars LN E2 ==>
50+
?iv err vR vF m.
51+
FloverMapTree_find e A = SOME (iv,err) /\
52+
eval_expr E1 (toRTMap (toRExpMap Gamma)) (toREval e) vR REAL /\
53+
eval_expr E2 (toRExpMap Gamma) e vF m /\
54+
(!vF m.
55+
eval_expr E2 (toRExpMap Gamma) e vF m ==>
56+
abs (vR - vF) <= err /\ validFloatValue vF m)
57+
Proof
58+
(**
59+
The proofs is a simple composition of the soundness proofs for the range
60+
validator and the error bound validator.
61+
**)
62+
simp [CertificateChecker_def]
63+
\\ rpt strip_tac
64+
\\ Cases_on `getValidMap defVars e FloverMapTree_empty` \\ fs[]
65+
\\ IMP_RES_TAC getValidMap_top_correct
66+
\\ rveq
67+
\\ `validTypes e Gamma`
68+
by (first_x_assum irule
69+
\\ fs[FloverMapTree_empty_def, FloverMapTree_mem_def, FloverMapTree_find_def])
70+
\\ drule validIntervalbounds_sound
71+
\\ rpt (disch_then drule)
72+
\\ disch_then (qspecl_then [`fVars`,`E1`, `Gamma`] destruct)
73+
\\ fs[dVars_range_valid_def, fVars_P_sound_def]
74+
\\ drule validErrorbound_sound
75+
\\ rpt (disch_then drule)
76+
\\ IMP_RES_TAC validRanges_single
77+
\\ disch_then (qspecl_then [`vR`, `err`, `FST iv`, `SND iv`] destruct)
78+
\\ fs[]
79+
\\ rpt (find_exists_tac \\ fs[])
80+
\\ rpt strip_tac
81+
>- (first_x_assum irule \\ fs[]
82+
\\ asm_exists_tac \\ fs[])
83+
\\ drule FPRangeValidator_sound
84+
\\ rpt (disch_then drule)
85+
\\ disch_then irule \\ fs[]
86+
QED
87+
88+
Definition CertificateCheckerCmd_def:
89+
CertificateCheckerCmd (f:real cmd) (absenv:analysisResult) (P:precond)
90+
defVars =
91+
(case getValidMapCmd defVars f FloverMapTree_empty of
92+
| Fail _ => NONE
93+
| FailDet _ _ => NONE
94+
| Succes Gamma =>
95+
if (validSSA f (freeVars f))
96+
then
97+
if ((validIntervalboundsCmd f absenv P LN) /\
98+
FPRangeValidatorCmd f absenv Gamma LN)
99+
then
100+
if validErrorboundCmd f Gamma absenv LN
101+
then SOME Gamma
102+
else NONE
103+
else NONE
104+
else NONE)
105+
End
106+
107+
Theorem CertificateCmd_checking_is_sound:
108+
!(f:real cmd) (A:analysisResult) (P:precond) defVars
109+
(E1 E2:env) (fVars:num_set) Gamma.
110+
(!v.
111+
v IN (domain (freeVars f)) ==>
112+
?vR.
113+
(E1 v = SOME vR) /\
114+
FST (P v) <= vR /\ vR <= SND (P v)) /\
115+
domain (freeVars f) SUBSET (domain fVars) /\
116+
CertificateCheckerCmd f A P defVars = SOME Gamma /\
117+
approxEnv E1 (toRExpMap Gamma) A (freeVars f) LN E2 ==>
118+
?iv err vR vF m.
119+
FloverMapTree_find (getRetExp f) A = SOME (iv, err) /\
120+
bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
121+
bstep f E2 (toRExpMap Gamma) vF m /\
122+
(!vF m. bstep f E2 (toRExpMap Gamma) vF m ==> abs (vR - vF) <= err)
123+
Proof
124+
simp [CertificateCheckerCmd_def]
125+
\\ rpt strip_tac
126+
\\ Cases_on `getValidMapCmd defVars f FloverMapTree_empty` \\ fs[]
127+
\\ rveq \\ imp_res_tac getValidMapCmd_correct
128+
\\ `validTypesCmd f Gamma`
129+
by (first_x_assum irule
130+
\\ fs[FloverMapTree_empty_def, FloverMapTree_mem_def, FloverMapTree_find_def])
131+
\\ `?outVars. ssa f (freeVars f) outVars` by (match_mp_tac validSSA_sound \\ fs[])
132+
\\ qspecl_then
133+
[`f`, `A`, `E1`, `freeVars f`, `LN`, `outVars`, `P`, `Gamma`]
134+
destruct validIntervalboundsCmd_sound
135+
\\ fs[dVars_range_valid_def, fVars_P_sound_def]
136+
\\ IMP_RES_TAC validRangesCmd_single
137+
\\ qspecl_then
138+
[`f`, `A`, `E1`, `E2`, `outVars`, `freeVars f`, `LN`, `vR`, `FST iv_e`,
139+
`SND iv_e`, `err_e`, `m`, `Gamma`]
140+
destruct validErrorboundCmd_gives_eval
141+
\\ fs[]
142+
\\ rpt (find_exists_tac \\ fs[])
143+
\\ rpt strip_tac
144+
\\ drule validErrorboundCmd_sound
145+
\\ rpt (disch_then drule)
146+
\\ rename1 `bstep f E2 _ vF2 m2`
147+
\\ disch_then
148+
(qspecl_then
149+
[`outVars`, `vR`, `vF2`, `FST iv_e`, `SND iv_e`, `err_e`, `m2`] destruct)
150+
\\ fs[]
151+
QED
152+
153+
Theorem CertificateCheckerCmd_Gamma_is_getValidMapCmd:
154+
CertificateCheckerCmd f A P dVars = SOME Gamma ⇒
155+
getValidMapCmd dVars f FloverMapTree_empty = Succes Gamma
156+
Proof
157+
fs[CertificateCheckerCmd_def]
158+
\\ rpt (TOP_CASE_TAC \\ fs[])
159+
QED
160+
161+
val _ = export_theory();

‎icing/flover/CertificateGeneratorScript.sml

+48
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
open RealIntervalInferenceTheory ErrorIntervalInferenceTheory ExpressionsTheory
2+
FloverMapTheory TypeValidatorTheory CommandsTheory AbbrevsTheory
3+
ExpressionAbbrevsTheory;
4+
open preambleFloVer;
5+
6+
val _ = new_theory "CertificateGenerator";
7+
8+
val CertificateGeneratorExp_def = Define `
9+
CertificateGeneratorExp (f:real expr) (P:precond) (Gamma:typeMap)
10+
:(real expr # precond # typeMap # analysisResult) option =
11+
let
12+
ivMap = inferIntervalbounds f P FloverMapTree_empty;
13+
fullTMap = getValidMap Gamma f FloverMapTree_empty;
14+
in
15+
case ivMap, fullTMap of
16+
| SOME ivMap, Succes tMap =>
17+
(case inferErrorbound f tMap ivMap FloverMapTree_empty of
18+
| SOME errMap => SOME (f,P,Gamma,errMap)
19+
| NONE => NONE)
20+
| _, _ => NONE`;
21+
22+
val getExp_def = Define `
23+
getExp (f, P, Gamma, errMap) = f`;
24+
25+
val getError_def = Define `
26+
getError (f, P, Gamma, errMap) = FloverMapTree_find f errMap`;
27+
28+
val CertificateGeneratorCmd_def = Define `
29+
CertificateGeneratorCmd (f:real cmd) (P:precond) (Gamma:typeMap)
30+
:(real cmd # precond # typeMap # analysisResult) option =
31+
let
32+
ivMap = inferIntervalboundsCmd f P FloverMapTree_empty;
33+
fullTMap = getValidMapCmd Gamma f FloverMapTree_empty;
34+
in
35+
case ivMap, fullTMap of
36+
| SOME ivMap, Succes tMap =>
37+
(case inferErrorboundCmd f tMap ivMap FloverMapTree_empty of
38+
| SOME errMap => SOME (f,P,Gamma,errMap)
39+
| NONE => NONE)
40+
| _, _ => NONE`;
41+
42+
val getCmd_def = Define `
43+
getCmd (f, P, Gamma, errMap) = f`;
44+
45+
val getError_def = Define `
46+
getError (f, P, Gamma, errMap) = FloverMapTree_find (getRetExp f) errMap`;
47+
48+
val _ = export_theory ();

‎icing/flover/EnvironmentsScript.sml

+158
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,158 @@
1+
open simpLib realTheory realLib RealArith sptreeTheory;
2+
open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory
3+
FloverTactics FloverMapTheory MachineTypeTheory;
4+
open preambleFloVer;
5+
6+
val _ = new_theory "Environments";
7+
8+
val _ = temp_overload_on("abs",``real$abs``);
9+
10+
Definition approxEnv_def:
11+
approxEnv E1 Gamma absEnv (fVars:num_set) (dVars:num_set) E2 =
12+
((* No variable defined twice *)
13+
domain fVars INTER domain dVars = EMPTY ∧
14+
(* environments are only defined for the domain *)
15+
(∀ x. ~ (x IN (domain fVars UNION domain dVars)) ⇒
16+
E1 x = NONE ∧ E2 x = NONE) ∧
17+
(* All free variables are bounded in error by their machine epsilon *)
18+
(∀ x. x IN domain fVars ⇒
19+
∃ m v1 v2.
20+
Gamma (Var x) = SOME m ∧
21+
E1 x = SOME v1 ∧
22+
E2 x = SOME v2 ∧
23+
abs (v1 - v2) ≤ computeError v1 m) ∧
24+
(* All bound variables are bounded in error by their inferred bound *)
25+
(∀ x. x IN domain dVars ⇒
26+
∃ m iv err v1 v2.
27+
Gamma (Var x) = SOME m ∧
28+
E1 x = SOME v1 ∧
29+
E2 x = SOME v2 ∧
30+
FloverMapTree_find (Var x) absEnv = SOME (iv, err) ∧
31+
abs (v1 - v2) ≤ err))
32+
End
33+
34+
Theorem approxEnvRefl:
35+
approxEnv emptyEnv Gamma A LN LN emptyEnv
36+
Proof
37+
simp[approxEnv_def]
38+
QED
39+
40+
Theorem approxEnvUpdFree:
41+
(!(E1:env) (E2:env) (Gamma: real expr -> mType option) (A:analysisResult)
42+
(fVars:num_set) (dVars:num_set) v1 v2 x.
43+
approxEnv E1 Gamma A fVars dVars E2 /\
44+
(Gamma (Var x) = SOME m) /\
45+
(abs (v1 - v2) <= computeError v1 m) /\
46+
(lookup x (union fVars dVars) = NONE) ==>
47+
approxEnv (updEnv x v1 E1)
48+
Gamma A (insert x () fVars) dVars
49+
(updEnv x v2 E2))
50+
Proof
51+
rw[] \\ fs[approxEnv_def] \\ rpt conj_tac
52+
>- (
53+
fs[EXTENSION, lookup_union, option_case_eq]
54+
\\ CCONTR_TAC \\ fs[] \\ rveq
55+
\\ metis_tac[domain_lookup])
56+
>- (
57+
rpt strip_tac \\ rveq \\ res_tac
58+
\\ fsrw_tac [SATISFY_ss] []
59+
\\ ‘x' ≠ x’
60+
by (CCONTR_TAC \\ fs[] \\ rveq
61+
\\ fs[lookup_union, option_case_eq, domain_lookup])
62+
\\ fs[])
63+
\\ rpt strip_tac \\ res_tac \\ fsrw_tac [SATISFY_ss] []
64+
\\ ‘x' ≠ x’
65+
by (CCONTR_TAC \\ fs[] \\ rveq
66+
\\ fs[lookup_union, option_case_eq, domain_lookup])
67+
\\ fs[]
68+
QED
69+
70+
Theorem approxEnvUpdBound:
71+
∀ (E1:env) (E2:env) (Gamma: real expr -> mType option) (A:analysisResult)
72+
(fVars:num_set) (dVars:num_set) v1 v2 x iv err.
73+
approxEnv E1 Gamma A fVars dVars E2 /\
74+
Gamma (Var x) = SOME m /\
75+
FloverMapTree_find (Var x) A = SOME (iv,err) /\
76+
abs (v1 - v2) <= err /\
77+
(lookup x (union fVars dVars) = NONE) ==>
78+
approxEnv (updEnv x v1 E1)
79+
Gamma A fVars (insert x () dVars)
80+
(updEnv x v2 E2)
81+
Proof
82+
rw[] \\ fs[approxEnv_def] \\ rpt conj_tac
83+
>- (
84+
fs[EXTENSION, lookup_union, option_case_eq]
85+
\\ CCONTR_TAC \\ fs[] \\ rveq
86+
\\ metis_tac[domain_lookup])
87+
>- (
88+
rpt strip_tac \\ rveq \\ res_tac
89+
\\ fsrw_tac [SATISFY_ss] []
90+
\\ ‘x' ≠ x’
91+
by (CCONTR_TAC \\ fs[] \\ rveq
92+
\\ fs[lookup_union, option_case_eq, domain_lookup])
93+
\\ fs[])
94+
\\ rpt strip_tac \\ res_tac \\ fsrw_tac [SATISFY_ss] []
95+
\\ ‘x' ≠ x’
96+
by (CCONTR_TAC \\ fs[] \\ rveq
97+
\\ fs[lookup_union, option_case_eq, domain_lookup])
98+
\\ fs[]
99+
QED
100+
101+
val approxEnv_rules = LIST_CONJ [approxEnvRefl, approxEnvUpdFree, approxEnvUpdBound]
102+
val _ = save_thm ("approxEnv_rules", approxEnv_rules);
103+
104+
Theorem approxEnv_gives_value:
105+
!E1 E2 x v (fVars:num_set) (dVars:num_set) absenv Gamma.
106+
approxEnv E1 Gamma absenv fVars dVars E2 /\
107+
E1 x = SOME v /\
108+
x IN ((domain fVars) UNION (domain dVars)) ==>
109+
?v2. E2 x = SOME v2
110+
Proof
111+
rw[approxEnv_def] \\ res_tac \\ fsrw_tac [SATISFY_ss] []
112+
QED
113+
114+
Theorem approxEnv_fVar_bounded:
115+
!E1 Gamma absenv fVars dVars E2 x v v2 m.
116+
approxEnv E1 Gamma absenv fVars dVars E2 /\
117+
E1 x = SOME v /\
118+
E2 x = SOME v2 /\
119+
x IN (domain fVars) /\
120+
Gamma (Var x) = SOME m ==>
121+
abs (v - v2) <= computeError v m
122+
Proof
123+
rw[approxEnv_def] \\ res_tac \\ fs[]
124+
\\ metis_tac[]
125+
QED
126+
127+
Theorem approxEnv_dVar_bounded:
128+
!E1 (Gamma:real expr -> mType option) (A:analysisResult) fVars dVars E2 x v v2 m iv e.
129+
approxEnv E1 Gamma A fVars dVars E2 /\
130+
E1 x = SOME v /\
131+
E2 x = SOME v2 /\
132+
x IN (domain dVars) /\
133+
Gamma (Var x) = SOME m /\
134+
FloverMapTree_find (Var x) A = SOME (iv, e) ==>
135+
abs (v - v2) <= e
136+
Proof
137+
rw[approxEnv_def] \\ res_tac \\ fs[]
138+
\\ metis_tac[]
139+
QED
140+
141+
Theorem approxEnv_refl:
142+
∀ fVars dVars E1 Gamma A.
143+
(domain fVars INTER domain dVars = EMPTY) ∧
144+
(∀ x. x IN (domain fVars) UNION (domain dVars) ⇒
145+
∃ v. E1 x = SOME v) ∧
146+
(∀ x. ~ (x IN (domain fVars) UNION (domain dVars)) ⇒
147+
E1 x = NONE) ∧
148+
(∀ x. x IN (domain dVars) ⇒ ∃ err iv. FloverMapTree_find (Var x) A = SOME (iv, err) ∧ 0 ≤ err) ∧
149+
(∀ x. x IN (domain fVars) UNION (domain dVars) ⇒
150+
∃ m. Gamma (Var x) = SOME m) ⇒
151+
approxEnv E1 Gamma A fVars dVars E1
152+
Proof
153+
rw[approxEnv_def] \\ res_tac \\ fsrw_tac [SATISFY_ss] []
154+
\\ Cases_on ‘m’ \\ fs[mTypeToR_pos]
155+
\\ irule computeError_pos
156+
QED
157+
158+
val _ = export_theory ();;

0 commit comments

Comments
 (0)