Commit 7a7f427d authored by Nikita Zyuzin's avatar Nikita Zyuzin

Set up integration of affine validator into range validator

parent 0a50d6e2
......@@ -462,7 +462,7 @@ Proof.
lra.
Qed.
Definition dVars_range_valid (dVars: NatSet.t) (E: env) (A: analysisResult): Prop :=
Definition affine_dVars_range_valid (dVars: NatSet.t) (E: env) (A: analysisResult): Prop :=
forall v map1 noise exprAfs, NatSet.In v dVars ->
exists map2 af vR iv err,
contained_map map1 map2 /\
......@@ -474,7 +474,7 @@ Definition dVars_range_valid (dVars: NatSet.t) (E: env) (A: analysisResult): Pro
E v = Some vR /\
af_evals (afQ2R af) vR map2.
Definition fVars_P_sound (fVars: NatSet.t) (E: env) (P: precond): Prop :=
Definition affine_fVars_P_sound (fVars: NatSet.t) (E: env) (P: precond): Prop :=
forall v map1 noise,
NatSet.In v fVars ->
exists vR map2, E v = Some vR /\
......@@ -482,8 +482,7 @@ Definition fVars_P_sound (fVars: NatSet.t) (E: env) (P: precond): Prop :=
(forall n, (n >= noise)%nat -> map2 n = None) /\
af_evals (afQ2R (fromIntv (P v) noise)) vR map2.
Definition vars_typed (S: NatSet.t) (Gamma: nat -> option mType) :=
Definition affine_vars_typed (S: NatSet.t) (Gamma: nat -> option mType) :=
forall v, NatSet.In v S ->
exists m: mType, Gamma v = Some m.
......@@ -504,10 +503,10 @@ Lemma validAffineBounds_sound (e: exp Q) (A: analysisResult) (P: precond)
(inoise > 0)%nat ->
(forall n, (n >= inoise)%nat -> map1 n = None) ->
validAffineBounds e A P dVars iexpmap inoise = Some (exprAfs, noise) ->
dVars_range_valid dVars E A ->
affine_dVars_range_valid dVars E A ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
fVars_P_sound fVars E P ->
vars_typed (NatSet.union fVars dVars) Gamma ->
affine_fVars_P_sound fVars E P ->
affine_vars_typed (NatSet.union fVars dVars) Gamma ->
exists map2 af vR aiv aerr,
contained_map map1 map2 /\
FloverMap.find e A = Some (aiv, aerr) /\
......
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Flover.Infra.RealSimps Flover.Infra.RationalSimps Flover.Infra.RealRationalProps Flover.Infra.Ltacs.
Require Export Flover.IntervalValidation.
Require Import Flover.Infra.RealSimps Flover.Infra.RationalSimps Flover.Infra.RealRationalProps Flover.Infra.Ltacs Flover.AffineForm.
Require Export Flover.IntervalValidation Flover.AffineValidation.
Require Export Coq.QArith.QArith.
Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.
Definition RangeValidator e A P :=
(*if*)
validIntervalbounds e A P NatSet.empty.
(*then true
match validAffineBounds e A P NatSet.empty with
| Some (p, b) => b
| None => false
end.
else validAffineBounds e A P NatSet.empty*)
if
validIntervalbounds e A P NatSet.empty
then true
else match validAffineBounds e A P NatSet.empty (FloverMap.empty (affine_form Q)) 1 with
| Some _ => true
| None => false
end.
Theorem RangeValidator_sound (f : exp Q) (A : analysisResult) (P : precond)
(E : env) (Gamma : nat -> option mType) :
......@@ -25,8 +24,16 @@ Theorem RangeValidator_sound (f : exp Q) (A : analysisResult) (P : precond)
Proof.
intros.
unfold RangeValidator in *.
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.
destruct (validIntervalbounds f A P NatSet.empty) 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.
- destruct (validAffineBounds f A P NatSet.empty (FloverMap.empty (affine_form Q)) 1) eqn: Hafcheck;
try congruence.
clear H.
destruct p as [exprAfs noise].
pose proof (validAffineBounds_sound) as sound_affine.
specialize (sound_affine f A P NatSet.empty NatSet.empty E Gamma
exprAfs noise (FloverMap.empty (affine_form Q)) 1%nat (fun _ => None)).
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