Commit 9421bbb5 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Ensure compilation of RealRangeValidator

parent 6dbb5327
......@@ -57,6 +57,10 @@ Proof.
assert (dVars_range_valid NatSet.empty E1 absenv).
{ unfold dVars_range_valid.
intros; set_tac. }
assert (affine_dVars_range_valid NatSet.empty E1 absenv 1 (FloverMap.empty _) (fun _ => None))
as affine_dvars_valid.
{ unfold affine_dVars_range_valid.
intros; set_tac. }
assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
{ hnf; intros a in_empty.
set_tac. }
......@@ -64,7 +68,7 @@ Proof.
{ unfold vars_typed. intros; apply types_defined. set_tac. destruct H1; set_tac.
split; try auto. hnf; intros; set_tac. }
rename R into validFPRanges.
edestruct (RangeValidator_sound e absenv (P:=P) (Gamma:=defVars) (E:=E1))
edestruct (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=defVars) (E:=E1))
as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]]; eauto.
destruct iv_e as [elo ehi].
edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType)) L approxE1E2 H0 eval_real R0 L1 H P_valid H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
......@@ -75,7 +79,7 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) d
let tMap := typeMapCmd defVars f (FloverMap.empty mType) in
if (typeCheckCmd f defVars tMap && validSSA f (freeVars f))
then
if (validIntervalboundsCmd f absenv P NatSet.empty) &&
if (RangeValidatorCmd f absenv P NatSet.empty) &&
FPRangeValidatorCmd f absenv tMap NatSet.empty
then (validErrorboundCmd f tMap absenv NatSet.empty)
else false
......@@ -130,4 +134,4 @@ Proof.
split; try auto; split; try auto.
intros.
eapply validErrorboundCmd_sound; eauto.
Qed.
\ No newline at end of file
Qed.
......@@ -17,7 +17,7 @@ Theorem RangeValidator_sound (f : expr Q) (A : analysisResult) (P : precond) dVa
(E : env) (Gamma : nat -> option mType) :
RangeValidator f A P dVars = true ->
dVars_range_valid dVars E A ->
affine_dVars_range_valid
affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
fVars_P_sound (usedVars f) E P ->
vars_typed (NatSet.union (usedVars f) dVars) Gamma ->
exists (iv : intv) (err : error) (vR : R),
......@@ -32,7 +32,7 @@ Proof.
- pose (iexpmap := (FloverMap.empty (affine_form Q))).
pose (inoise := 1%nat).
epose (imap := (fun _ : nat => None)).
fold iexpmap inoise imap in H.
fold iexpmap inoise imap in H, H1.
destruct (validAffineBounds f A P dVars iexpmap inoise) eqn: Hafcheck;
try congruence.
clear H.
......@@ -40,24 +40,19 @@ Proof.
pose proof (validAffineBounds_sound) as sound_affine.
assert ((forall e : FloverMap.key,
(exists af : affine_form Q, FloverMap.find (elt:=affine_form Q) e iexpmap = Some af) ->
checked_expressions A E Gamma (usedVars f) NatSet.empty e iexpmap inoise imap)) as Hchecked
checked_expressions A E Gamma (usedVars f) dVars e iexpmap inoise imap)) as Hchecked
by (intros e Hein; destruct Hein as [af Hein]; unfold iexpmap in Hein;
rewrite FloverMapFacts.P.F.empty_o in Hein;
congruence).
assert (1 > 0)%nat as Hinoise by omega.
eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
assert (affine_dVars_range_valid dVars E A inoise iexpmap imap).
{ unfold affine_dVars_range_valid.
as HdVarsValid
by (unfold affine_dVars_range_valid; intros * H; set_tac).
assert (NatSet.Subset (usedVars f -- NatSet.empty) (usedVars f)) as Hsubset by set_tac.
assert (affine_fVars_P_sound (usedVars f) E P) as HfVars by exact H0.
assert (affine_vars_typed (usedVars f NatSet.empty) Gamma) as Hvarstyped
by (unfold affine_vars_typed; intros v in_set; set_tac; destruct in_set; set_tac).
specialize (sound_affine f A P (usedVars f) NatSet.empty E Gamma
assert (NatSet.Subset (usedVars f -- dVars) (usedVars f)) as Hsubset by set_tac.
assert (affine_fVars_P_sound (usedVars f) E P) as HfVars by exact H2.
assert (affine_vars_typed (usedVars f dVars) Gamma) as Hvarstyped
by exact H3.
specialize (sound_affine f A P (usedVars f) dVars E Gamma
exprAfs noise iexpmap inoise imap
Hchecked Hinoise Himap Hafcheck HdVarsValid Hsubset HfVars Hvarstyped)
Hchecked Hinoise Himap Hafcheck H1 Hsubset HfVars Hvarstyped)
as [map2 [af [vR [aiv [aerr sound_affine]]]]].
destruct sound_affine as [_ [_ [Haiv [Hsup [_ [_ [_ [_ [Hee [Heval _]]]]]]]]]].
exists aiv, aerr, vR.
......@@ -73,4 +68,25 @@ Proof.
simpl in Heval.
destruct Heval as [Heval1 Heval2].
split; eauto using Rle_trans.
Qed.
\ No newline at end of file
Qed.
Definition RangeValidatorCmd e A P dVars:=
if
validIntervalboundsCmd e A P dVars
then true
else match validAffineBoundsCmd e A P dVars (FloverMap.empty (affine_form Q)) 1 with
| Some _ => true
| None => false
end.
Theorem RangeValidatorCmd_sound (c : cmd Q) (A : analysisResult) (P : precond) dVars
(E : env) (Gamma : nat -> option mType) :
RangeValidatorCmd c A P dVars = true ->
ssa f (NatSet.union fVars dVars) outVars ->
dVars_range_valid dVars E A ->
affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
fVars_P_sound (usedVars f) E P ->
vars_typed (NatSet.union (usedVars f) dVars) Gamma ->
exists (iv : intv) (err : error) (vR : R),
FloverMap.find (elt:=intv * error) f A = Some (iv, err) /\
bstep (toREvalCmd (toRCmd c)) E (toRMap Gamma) vR REAL /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
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