Commit 45996163 authored by Joachim Bard's avatar Joachim Bard

adding affine interval checker again

parent a6535678
......@@ -63,10 +63,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.
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. } *)
intros; set_tac. }
assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
{ hnf; intros a in_empty.
set_tac. }
......@@ -157,8 +157,8 @@ Proof.
as freeVars_contained by set_tac.
assert (validRangesCmd f absenv E1 (toRTMap (toRExpMap Gamma))) as valid_f.
{ eapply (RangeValidatorCmd_sound _ (fVars:=preVars P)); eauto; intuition.
(* unfold affine_dVars_range_valid; intros.
set_tac. *) }
unfold affine_dVars_range_valid; intros.
set_tac. }
pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
destruct iv as [f_lo f_hi].
......
......@@ -8,28 +8,23 @@ From Flover
From Coq Require Export QArith.QArith.
From Flover
Require Export IntervalValidation SMTArith SMTValidation RealRangeArith
Infra.ExpressionAbbrevs Commands.
(* TODO: add AffineValidation again to the export part after it is
adjusted to the new precond type *)
Require Export IntervalValidation AffineValidation SMTArith SMTValidation
RealRangeArith Infra.ExpressionAbbrevs Commands.
Definition RangeValidator e A P Qmap dVars :=
if
validIntervalbounds e A P dVars
then true
else validSMTIntervalbounds e A P Qmap dVars.
(*
else match validAffineBounds e A P dVars (FloverMap.empty (affine_form Q)) 1 with
| Some _ => true
| None => false
| None => validSMTIntervalbounds e A P Qmap dVars
end.
*)
Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : precond)
Qmap dVars (E : env) (Gamma : FloverMap.t mType):
RangeValidator e A P Qmap dVars = true ->
dVars_range_valid dVars E A ->
(* affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) -> *)
affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
validTypes e Gamma ->
eval_precond E P ->
unsat_queries E Qmap ->
......@@ -40,14 +35,12 @@ Proof.
destruct (validIntervalbounds e A P dVars) eqn: Hivcheck.
- eapply validIntervalbounds_sound; set_tac; eauto.
(* unfold dVars_range_valid; intros; set_tac. *)
- eapply validSMTIntervalbounds_sound; set_tac; eauto.
(*
- pose (iexpmap := (FloverMap.empty (affine_form Q))).
pose (inoise := 1%nat).
epose (imap := (fun _ : nat => None)).
fold iexpmap inoise imap in H, H1.
destruct (validAffineBounds e A P dVars iexpmap inoise) eqn: Hafcheck;
try congruence.
try now (eapply validSMTIntervalbounds_sound; set_tac; eauto).
clear H.
destruct p as [exprAfs noise].
pose proof (validAffineBounds_sound) as sound_affine.
......@@ -60,28 +53,21 @@ Proof.
assert (1 > 0)%nat as Hinoise by omega.
eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
assert (NatSet.Subset (usedVars e -- dVars) (usedVars e)) as Hsubset by set_tac.
assert (fVars_P_sound (usedVars e) E P) as HfVars by exact H3.
rename H3 into Hpre.
specialize (sound_affine e A P (usedVars e) dVars E Gamma
exprAfs noise iexpmap inoise imap
Hchecked Hinoise Himap Hafcheck H1 Hsubset HfVars)
Hchecked Hinoise Himap Hafcheck H1 Hsubset Hpre)
as [map2 [af [vR [aiv [aerr sound_affine]]]]]; intuition.
*)
Qed.
Definition RangeValidatorCmd e A P Qmap dVars:=
if
validIntervalboundsCmd e A P dVars
then true
else validSMTIntervalboundsCmd e A P Qmap 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
| None => validSMTIntervalboundsCmd e A P Qmap dVars
end.
*)
Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond)
(Qmap: usedQueries) dVars
......@@ -89,7 +75,7 @@ Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond)
RangeValidatorCmd f A P Qmap 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) -> *)
affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
eval_precond E P ->
NatSet.Subset (preVars P) fVars ->
NatSet.Subset (freeVars f -- dVars) fVars ->
......@@ -101,14 +87,12 @@ Proof.
unfold RangeValidatorCmd in ranges_valid.
destruct (validIntervalboundsCmd f A P dVars) eqn:iv_valid.
- eapply validIntervalboundsCmd_sound; eauto.
- eapply validSMTIntervalboundsCmd_sound; eauto.
(*
- pose (iexpmap := (FloverMap.empty (affine_form Q))).
pose (inoise := 1%nat).
epose (imap := (fun _ : nat => None)).
fold iexpmap inoise imap in ranges_valid, H1.
destruct (validAffineBoundsCmd f A P dVars iexpmap inoise) eqn: Hafcheck;
try congruence.
try now (eapply validSMTIntervalboundsCmd_sound; eauto).
destruct p as [exprAfs noise].
pose proof (validAffineBoundsCmd_sound) as sound_affine.
assert ((forall e' : FloverMap.key,
......@@ -119,10 +103,8 @@ 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 (fVars_P_sound fVars E P) as HfVars by exact H2.
specialize (sound_affine f A P fVars dVars outVars E Gamma
exprAfs noise iexpmap inoise imap
Hchecked Hinoise Himap Hafcheck H H1 H3 HfVars)
Hchecked Hinoise Himap Hafcheck H H1 H4 H3 H2)
as [map2 [af [vR [aiv [aerr sound_affine]]]]]; intuition.
*)
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