Commit a15e51d7 authored by Heiko Becker's avatar Heiko Becker

Start working on validRanges predicate, necessary to fix issues with new validators

parent 9421bbb5
This diff is collapsed.
......@@ -231,14 +231,24 @@ Definition checked_error_expressions (A: analysisResult) (E1 E2:env) Gamma e
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) -> *)
Theorem validErrorboundAA_sound e:
forall E1 E2 P Gamma defVars nR A elo ehi tMap fVars dVars currNoise maxNoise initMap resMap M1,
(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 ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
affine_dVars_range_valid dVars E1 A currNoise initMap M1 ->
affine_fVars_P_sound fVars E1 P ->
affine_vars_typed fVars Gamma ->
validErrorboundAA e Gamma A tMap currNoise initMap = Some (resMap, maxNoise) ->
RangeValidator e A P dVars = true ->
typeCheck e defVars Gamma = true ->
vars_typed (NatSet.union fVars dVars) defVars ->
FloverMap.find e A = Some ((elo,ehi),err) ->
(exists nF m,
eval_expr E2 defVars (toRExp e) nF m) /\
(forall nF m,
eval_expr E2 defVars (toRExp e) nF m ->
(Rabs (nR - nF) <= (Q2R err))%R).
This diff is collapsed.
From Coq
Require Import QArith.QArith QArith.Qreals QArith.Qminmax micromega.Psatz.
From Flover
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Infra.Ltacs Infra.RealSimps Typing IntervalArithQ IntervalArith Commands.
Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop :=
forall v, NatSet.In v dVars ->
exists vR iv err,
E v = Some vR /\
FloverMap.find (Var Q v) A = Some (iv, err) /\
(Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Definition fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop :=
forall v,
NatSet.In v fVars ->
exists vR, E v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R.
Definition vars_typed (S:NatSet.t) (Gamma: nat -> option mType) :=
forall v, NatSet.In v S ->
exists m :mType, Gamma v = Some m.
Ltac kill_trivial_exists :=
match goal with
| [ |- exists iv err v, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e
| [ |- exists iv err, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e
end.
Fixpoint validRanges e (A:analysisResult) E Gamma :Prop :=
match e with
| Var _ x => True
| Const m v => True
| Unop u e1 => validRanges e1 A E Gamma
| Binop b e1 e2 =>
(b = Div ->
(forall iv2 err,
FloverMap.find e2 A = Some (iv2, err) ->
((Qleb (ivhi iv2) 0) && (negb (Qeq_bool (ivhi iv2) 0))) ||
((Qleb 0 (ivlo iv2)) && (negb (Qeq_bool (ivlo iv2) 0))) = true)) /\
validRanges e1 A E Gamma /\ validRanges e2 A E Gamma
| Fma e1 e2 e3 =>
validRanges e1 A E Gamma /\ validRanges e2 A E Gamma /\ validRanges e3 A E Gamma
| Downcast m e1 => validRanges e1 A E Gamma
end /\
exists iv err vR,
FloverMap.find e A = Some (iv, err) /\
eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL /\
(Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Corollary validRanges_single e A E Gamma:
validRanges e A E Gamma ->
exists iv err vR,
FloverMap.find e A = Some (iv, err) /\
eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL /\
(Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Proof.
destruct e; intros [_ valid_e]; simpl in *; try auto.
Qed.
Lemma swap_Gamma_eval_expr e E vR m Gamma1 Gamma2:
(forall n, Gamma1 n = Gamma2 n) ->
eval_expr E Gamma1 e vR m ->
eval_expr E Gamma2 e vR m.
Proof.
revert E vR Gamma1 Gamma2 m;
induction e; intros * Gamma_eq eval_e;
inversion eval_e; subst; simpl in *;
try eauto.
apply Var_load; try auto.
rewrite <- Gamma_eq; auto.
Qed.
Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 :
(forall n, Gamma1 n = Gamma2 n) ->
bstep f E Gamma1 vR m ->
bstep f E Gamma2 vR m.
Proof.
revert E Gamma1 Gamma2;
induction f; intros * Gamma_eq eval_f.
- inversion eval_f; subst.
econstructor; try eauto.
+ eapply swap_Gamma_eval_expr; eauto.
+ apply (IHf _ (updDefVars n m0 Gamma1) _); try eauto.
intros n1.
unfold updDefVars.
case (n1 =? n); auto.
- inversion eval_f; subst.
econstructor; try eauto.
eapply swap_Gamma_eval_expr; eauto.
Qed.
Lemma validRanges_swap Gamma1 Gamma2:
forall e A E,
(forall n, (toRMap Gamma1) n = toRMap (Gamma2) n) ->
validRanges e A E Gamma1 ->
validRanges e A E Gamma2.
Proof.
induction e; intros * Gamma_swap valid1; simpl in *; try (split; auto);
try (
destruct valid1 as [_ [? [? [? [? [? ?]]]]]];
repeat eexists; eauto;
[eapply swap_Gamma_eval_expr with (Gamma1 := (toRMap Gamma1)); eauto |
lra |
lra]).
- destruct valid1; auto.
- destruct valid1 as [[? [? ?]] ?]; auto.
- admit.
- destruct valid1; auto.
Admitted.
Fixpoint validRangesCmd (f:cmd Q) A E Gamma {struct f} : Prop :=
match f with
| Let m x e g =>
validRanges e A E Gamma /\
(forall vR, eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL ->
validRangesCmd g A (updEnv x vR E) (updDefVars x REAL Gamma))
| Ret e => validRanges e A E Gamma
end /\
exists iv_e err_e vR,
FloverMap.find (getRetExp f) A = Some (iv_e, err_e) /\
bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR REAL /\
(Q2R (fst iv_e) <= vR <= Q2R (snd iv_e))%R.
Corollary validRangesCmd_single f A E Gamma:
validRangesCmd f A E Gamma ->
exists iv_e err_e vR,
FloverMap.find (getRetExp f) A = Some (iv_e, err_e) /\
bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR REAL /\
(Q2R (fst iv_e) <= vR <= Q2R (snd iv_e))%R.
Proof.
destruct f; simpl in *; intros [ _ valid_f]; auto.
Qed.
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Flover.Infra.RealSimps Flover.Infra.RationalSimps Flover.Infra.RealRationalProps Flover.Infra.Ltacs Flover.AffineForm.
Require Export Flover.IntervalValidation Flover.AffineValidation.
Require Export Flover.IntervalValidation Flover.AffineValidation Flover.RealRangeArith.
Require Export Coq.QArith.QArith.
Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.
......@@ -13,23 +13,23 @@ Definition RangeValidator e A P dVars:=
| None => false
end.
Theorem RangeValidator_sound (f : expr Q) (A : analysisResult) (P : precond) dVars
Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : precond) dVars
(E : env) (Gamma : nat -> option mType) :
RangeValidator f A P dVars = true ->
RangeValidator e A P dVars = true ->
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) /\
eval_expr E (toRMap Gamma) (toREval (toRExp f)) vR REAL /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
fVars_P_sound (usedVars e) E P ->
vars_typed (NatSet.union (usedVars e) dVars) Gamma ->
validRanges e A E Gamma.
Proof.
intros.
unfold RangeValidator in *.
destruct (validIntervalbounds f A P dVars) eqn: Hivcheck.
destruct (validIntervalbounds e A P dVars) eqn: Hivcheck.
- eapply validIntervalbounds_sound; eauto.
+ unfold dVars_range_valid; intros; set_tac.
- pose (iexpmap := (FloverMap.empty (affine_form Q))).
unfold dVars_range_valid; intros; set_tac.
- (* FIXME
@Nikita: Start here
pose (iexpmap := (FloverMap.empty (affine_form Q))).
pose (inoise := 1%nat).
epose (imap := (fun _ : nat => None)).
fold iexpmap inoise imap in H, H1.
......@@ -67,8 +67,8 @@ Proof.
rewrite <- to_interval_to_intv in Heval.
simpl in Heval.
destruct Heval as [Heval1 Heval2].
split; eauto using Rle_trans.
Qed.
split; eauto using Rle_trans. *)
Admitted.
Definition RangeValidatorCmd e A P dVars:=
if
......@@ -79,14 +79,20 @@ Definition RangeValidatorCmd e A P dVars:=
| 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 ->
Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond) dVars
(E : env) (Gamma : nat -> option mType) fVars outVars:
RangeValidatorCmd f 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.
fVars_P_sound fVars E P ->
vars_typed (NatSet.union fVars dVars) Gamma ->
NatSet.Subset (freeVars f -- dVars) fVars ->
validRangesCmd f A E Gamma.
Proof.
intros ranges_valid; intros.
unfold RangeValidatorCmd in ranges_valid.
destruct (validIntervalboundsCmd f A P dVars) eqn:iv_valid.
- eapply validIntervalboundsCmd_sound; eauto.
- (* FIXME *)
Admitted.
......@@ -27,7 +27,6 @@ forall (e : expr Q) (E1 E2 : env) (fVars dVars : NatSet.t) (A : analysisResult)
(exists (nF : R) (m : mType), eval_expr E2 defVars (toRExp e) nF m) /\
(forall (nF : R) (m : mType), eval_expr E2 defVars (toRExp e) nF m -> (Rabs (nR - nF) <= Q2R err)%R).
Proof.
intros.
cbn in *.
intros. cbn in *.
eapply validErrorbound_sound; eauto.
Qed.
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