Commit 6dbb5327 authored by Heiko Becker's avatar Heiko Becker

Start fixing compilation issues

parent c9bcf727
......@@ -16,7 +16,7 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (de
let tMap := (typeMap defVars e (FloverMap.empty mType)) in
if (typeCheck e defVars tMap)
then
if RangeValidator e absenv P && FPRangeValidator e absenv tMap NatSet.empty
if RangeValidator e absenv P NatSet.empty && FPRangeValidator e absenv tMap NatSet.empty
then RoundoffErrorValidator e tMap absenv NatSet.empty
else false
else false.
......
......@@ -218,3 +218,27 @@ Fixpoint validErrorboundAACmd (f:cmd Q) (* analyzed cmd with let's *)
end
|Ret e => validErrorboundAA e typeMap A dVars currNoise errMap
end.
Definition checked_error_expressions (A: analysisResult) (E1 E2:env) Gamma e
(initMap:FloverMap.t (affine_form Q)) currNoise (M1:noise_mapping) vR :=
eval_expr E1 (toRMap Gamma) (toREval (toRExp e)) vR REAL ->
exists (af:affine_form Q) (vF:R) m aiv aerr,
eval_expr E2 Gamma (toRExp e) vF m /\
FloverMap.find (elt:=intv * error) e A = Some (aiv, aerr) /\
FloverMap.find (elt:= affine_form Q) e initMap = Some af /\
fresh currNoise af /\
(forall n, (n >= currNoise)%nat -> M1 n = None) /\
let mAbs := maxAbs (toIntv af) in
(Rabs (vR - vF) <= (Q2R mAbs))%R.
(* Theorem validErrorboundAA_sound e: *)
(* forall E1 E2 P Gamma A tMap fVars dVars currNoise maxNoise initMap resMap, *)
(* (forall e vR, *)
(* FloverMap.In e initMap -> *)
(* checked_error_expressions A E1 E2 Gamma e initMap currNoise M1 vR) -> *)
(* approxEnv E1 defVars A fVars dVars E2 -> *)
(* affine_dVars_range_valid dVars E A currNoise initMap M1 -> *)
(* affine_fVars_P_sound fVars E P -> *)
(* affine_vars_typed fVars Gamma -> *)
(* validErrorboundAA e Gamma A tMap currNoise initMap = Some (resMap, maxNoise) -> *)
......@@ -4,36 +4,36 @@ Require Export Flover.IntervalValidation Flover.AffineValidation.
Require Export Coq.QArith.QArith.
Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.
Definition RangeValidator e A P :=
Definition RangeValidator e A P dVars:=
if
validIntervalbounds e A P NatSet.empty
validIntervalbounds e A P dVars
then true
else match validAffineBounds e A P NatSet.empty (FloverMap.empty (affine_form Q)) 1 with
else match validAffineBounds e A P dVars (FloverMap.empty (affine_form Q)) 1 with
| Some _ => true
| None => false
end.
Theorem RangeValidator_sound (f : expr Q) (A : analysisResult) (P : precond)
Theorem RangeValidator_sound (f : expr Q) (A : analysisResult) (P : precond) dVars
(E : env) (Gamma : nat -> option mType) :
RangeValidator f A P = true ->
RangeValidator f A P dVars = true ->
dVars_range_valid dVars E A ->
affine_dVars_range_valid
fVars_P_sound (usedVars f) E P ->
vars_typed (usedVars f) Gamma ->
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) /\
eval_expr E (toRMap Gamma) (toREval (toRExp f)) vR REAL /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Proof.
intros.
unfold RangeValidator in *.
destruct (validIntervalbounds f A P NatSet.empty) eqn: Hivcheck.
destruct (validIntervalbounds f A P dVars) eqn: Hivcheck.
- eapply validIntervalbounds_sound; eauto.
+ unfold dVars_range_valid; intros; set_tac.
+ set_tac.
+ unfold vars_typed. intros v in_set; set_tac. destruct in_set; set_tac.
- pose (iexpmap := (FloverMap.empty (affine_form Q))).
pose (inoise := 1%nat).
epose (imap := (fun _ : nat => None)).
fold iexpmap inoise imap in H.
destruct (validAffineBounds f A P NatSet.empty iexpmap inoise) eqn: Hafcheck;
destruct (validAffineBounds f A P dVars iexpmap inoise) eqn: Hafcheck;
try congruence.
clear H.
destruct p as [exprAfs noise].
......@@ -46,7 +46,10 @@ Proof.
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 NatSet.empty E A inoise iexpmap imap) as HdVarsValid
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.
......@@ -70,4 +73,4 @@ Proof.
simpl in Heval.
destruct Heval as [Heval1 Heval2].
split; eauto using Rle_trans.
Qed.
Qed.
\ No newline at end of file
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