Skip to content

GitLab

Commit aca4ef84 authored by Joachim Bard's avatar Joachim Bard
Browse files
Options

merging with IntervalChecker; some admits left

parent 48cc1d69
Hide whitespace changes
Inline Side-by-side
Showing with 121 additions and 106 deletions
coq/CertificateChecker.v
View file @ aca4ef84
......@@ -13,11 +13,11 @@ Require Export ExpressionSemantics Flover.Commands Coq.QArith.QArith.
(** Certificate checking function **)
Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
(P:precond) (defVars:FloverMap.t mType):=
(P:FloverMap.t intv) Qmap (defVars:FloverMap.t mType):=
let tMap := (getValidMap defVars e (FloverMap.empty mType)) in
match tMap with
|Succes tMap =>
if RangeValidator e absenv P NatSet.empty && FPRangeValidator e absenv tMap NatSet.empty
if RangeValidator e absenv P Qmap NatSet.empty && FPRangeValidator e absenv tMap NatSet.empty
then RoundoffErrorValidator e tMap absenv NatSet.empty
else false
| _ => false
......@@ -26,14 +26,13 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
(**
Soundness proof for the certificate checker.
Apart from assuming two executions, one in R and one on floats, we assume that
the real valued execution respects the precondition.
the real valued execution respects the precondition and dissatisfies the queries.
**)
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVars:
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap defVars:
forall (E1 E2:env),
(forall v, NatSet.In v (Expressions.usedVars e) ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
CertificateChecker e absenv P defVars = true ->
eval_precond (usedVars e) E1 P ->
unsat_queries E1 Qmap ->
CertificateChecker e absenv P Qmap defVars = true ->
exists Gamma,
approxEnv E1 (toRExpMap Gamma) absenv (usedVars e) NatSet.empty E2 ->
exists iv err vR vF m,
......@@ -48,7 +47,7 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVa
validator and the error bound validator.
**)
Proof.
intros * P_valid certificate_valid.
intros * P_valid unsat_qs certificate_valid.
unfold CertificateChecker in certificate_valid.
destruct (getValidMap defVars e (FloverMap.empty mType)) eqn:?; try congruence.
rename t into Gamma.
......@@ -72,7 +71,7 @@ Proof.
rename R0 into validFPRanges.
assert (validRanges e absenv E1 (toRTMap (toRExpMap Gamma))) as valid_e.
{ eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (E:=E1));
auto. }
eauto. }
pose proof (validRanges_single _ _ _ _ valid_e) as valid_single;
destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
destruct iv_e as [elo ehi].
......@@ -83,7 +82,7 @@ Proof.
exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto.
Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond)
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: FloverMap.t intv)
defVars :=
match getValidMapCmd defVars f (FloverMap.empty mType) with
| Succes Gamma =>
......@@ -97,12 +96,11 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond)
| _ => false
end.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P Qmap
defVars:
forall (E1 E2:env),
(forall v, NatSet.In v (freeVars f) ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
eval_precond (freeVars f) E1 P ->
unsat_queries E1 Qmap ->
CertificateCheckerCmd f absenv P defVars = true ->
exists Gamma,
approxEnv E1 (toRExpMap Gamma) absenv (freeVars f) NatSet.empty E2 ->
......@@ -118,7 +116,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
validator and the error bound validator.
**)
Proof.
intros * P_valid certificate_valid.
intros * P_valid unsat_qs certificate_valid.
unfold CertificateCheckerCmd in certificate_valid.
destruct (getValidMapCmd defVars f (FloverMap.empty mType)) eqn:?;
try congruence.
......
coq/IntervalValidation.v
View file @ aca4ef84
......@@ -145,15 +145,16 @@ Proof.
Qed.
Theorem validIntervalbounds_sound (f:expr Q) (A:analysisResult) (P: FloverMap.t intv)
dVars (E:env) Gamma:
fVars dVars (E:env) Gamma:
validIntervalbounds f A P dVars = true ->
dVars_range_valid dVars E A ->
eval_precond E P ->
NatSet.Subset ((Expressions.usedVars f) -- dVars) fVars ->
eval_precond fVars E P ->
validTypes f Gamma ->
validRanges f A E (toRTMap (toRExpMap Gamma)).
Proof.
induction f;
intros valid_bounds valid_definedVars valid_freeVars types_defined;
intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined;
cbn in *.
- destruct (NatSet.mem n dVars) eqn:?; cbn in *; split; auto.
+ destruct (valid_definedVars n)
......@@ -168,15 +169,14 @@ Proof.
match_simpl; auto.
+ Flover_compute.
destruct (valid_freeVars n i0) as [vR [env_valid bounds_valid]];
auto using find_in_precond.
canonize_hyps; simpl in *.
auto using find_in_precond; set_tac.
kill_trivial_exists.
eexists; split; [auto | split].
* econstructor; try eauto.
destruct types_defined as [m [find_m _]].
eapply toRExpMap_some in find_m; simpl; eauto.
match_simpl; auto.
* lra.
* canonize_hyps; cbn in *. lra.
- split; [auto |].
Flover_compute; canonize_hyps; simpl in *.
kill_trivial_exists.
......@@ -248,9 +248,9 @@ Proof.
- destruct types_defined
as [? [? [[? [? ?]]?]]].
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
by (Flover_compute; try congruence; apply IHf1; try auto).
by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
by (Flover_compute; try congruence; apply IHf2; try auto).
by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
repeat split;
[ intros; subst; Flover_compute; congruence |
auto | auto |].
......@@ -337,11 +337,11 @@ Proof.
- destruct types_defined
as [mG [find_mg [[validt_f1 [validt_f2 [validt_f3 valid_join]]] valid_exec]]].
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
by (Flover_compute; try congruence; apply IHf1; try auto).
by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
by (Flover_compute; try congruence; apply IHf2; try auto).
by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
assert (validRanges f3 A E (toRTMap (toRExpMap Gamma))) as valid_f3
by (Flover_compute; try congruence; apply IHf3; try auto).
by (Flover_compute; try congruence; apply IHf3; try auto; set_tac).
repeat split; try auto.
apply validRanges_single in valid_f1;
apply validRanges_single in valid_f2;
......@@ -394,30 +394,27 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
forall Gamma E fVars dVars outVars P,
ssa f (NatSet.union fVars dVars) outVars ->
dVars_range_valid dVars E A ->
eval_precond E P ->
(* NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> *)
eval_precond fVars E P ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
validIntervalboundsCmd f A P dVars = true ->
validTypesCmd f Gamma ->
validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
Proof.
induction f;
intros * ssa_f dVars_sound fVars_valid (* usedVars_subset *)
intros * ssa_f dVars_sound fVars_valid usedVars_subset
valid_bounds_f valid_types_f;
cbn in *.
- Flover_compute.
inversion ssa_f; subst.
canonize_hyps.
pose proof (validIntervalbounds_sound e Gamma (E:=E) L) as validIV_e.
pose proof (validIntervalbounds_sound e Gamma (E:=E) (fVars:=fVars) L) as validIV_e.
destruct valid_types_f
as [[mG [find_mG [_ [_ [validt_e validt_f]]]]] _].
assert (validRanges e A E (toRTMap (toRExpMap Gamma))) as valid_e
by now apply validIV_e.
(*
assert (validRanges e A E (toRTMap (toRExpMap Gamma))) as valid_e.
{ apply validIV_e; try auto.
set_tac. repeat split; auto.
hnf; intros; subst.
set_tac. }
*)
assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))).
{ hnf. intros a; split; intros in_set; set_tac.
- destruct in_set as [ ? | [? ?]]; try auto; set_tac.
......@@ -445,21 +442,15 @@ Proof.
congruence.
- hnf. intros x ? ?.
unfold updEnv.
case_eq (x =? n); intros case_x; try eapply fVars_valid; eauto.
case_eq (x =? n); intros case_x; auto.
rewrite Nat.eqb_eq in case_x. subst.
exists v. split; auto.
admit.
(*
assert (NatSet.In n (NatSet.union fVars dVars)) as in_union. set_tac.
assert (NatSet.In n (NatSet.union fVars dVars)) as in_union by set_tac.
exfalso; set_tac. apply H6; set_tac; auto.
*)
} (*
- intros x x_contained.
set_tac.
repeat split; try auto.
+ hnf; intros; subst. apply H1; set_tac.
+ hnf; intros. apply H1; set_tac. }
*)
(*
destruct x_contained as [x_free | x_def].
+ destruct (types_valid x) as [m_x Gamma_x]; try set_tac.
......@@ -502,11 +493,11 @@ Proof.
+ lra.
+ lra. }
- unfold validIntervalboundsCmd in valid_bounds_f.
pose proof (validIntervalbounds_sound e (E:=E) Gamma valid_bounds_f dVars_sound (* usedVars_subset*) ) as valid_iv_e.
pose proof (validIntervalbounds_sound e (E:=E) Gamma valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
destruct valid_types_f as [? ?].
assert (validRanges e A E (toRTMap (toRExpMap Gamma))) as valid_e by (apply valid_iv_e; auto).
split; try auto.
apply validRanges_single in valid_e.
destruct valid_e as [?[?[? [? [? ?]]]]]; try auto.
simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra.
Admitted.
Qed.
coq/RealRangeValidator.v
View file @ aca4ef84
......@@ -8,32 +8,39 @@ From Flover
From Coq Require Export QArith.QArith.
From Flover
Require Export IntervalValidation AffineValidation RealRangeArith
Require Export IntervalValidation AffineValidation SMTArith SMTValidation RealRangeArith
Infra.ExpressionAbbrevs Commands.
Definition RangeValidator e A P dVars:=
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
end.
*)
Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : precond) dVars
Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : FloverMap.t intv) Qmap dVars
(E : env) (Gamma : FloverMap.t mType):
RangeValidator e A P dVars = true ->
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) ->
validTypes e Gamma ->
fVars_P_sound (usedVars e) E P ->
eval_precond (usedVars e) E P ->
unsat_queries E Qmap ->
validRanges e A E (toRTMap (toRExpMap Gamma)).
Proof.
intros.
unfold RangeValidator in *.
destruct (validIntervalbounds e A P dVars) eqn: Hivcheck.
- eapply validIntervalbounds_sound; eauto.
unfold dVars_range_valid; intros; set_tac.
set_tac.
(* unfold dVars_range_valid; intros; set_tac. *)
- eapply validSMTIntervalbounds_sound; eauto; set_tac.
(*
- pose (iexpmap := (FloverMap.empty (affine_form Q))).
pose (inoise := 1%nat).
epose (imap := (fun _ : nat => None)).
......@@ -57,9 +64,12 @@ Proof.
exprAfs noise iexpmap inoise imap
Hchecked Hinoise Himap Hafcheck H1 Hsubset HfVars)
as [map2 [af [vR [aiv [aerr sound_affine]]]]]; intuition.
*)
Qed.
Definition RangeValidatorCmd e A P dVars:=
Definition RangeValidatorCmd e A P (* Qmap *) dVars:=
validIntervalboundsCmd e A P dVars.
(*
if
validIntervalboundsCmd e A P dVars
then true
......@@ -67,14 +77,15 @@ Definition RangeValidatorCmd e A P dVars:=
| Some _ => true
| None => false
end.
*)
Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond) dVars
Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : FloverMap.t intv) dVars
(E : env) Gamma 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 fVars E P ->
eval_precond fVars E P ->
NatSet.Subset (freeVars f -- dVars) fVars ->
validTypesCmd f Gamma ->
validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
......@@ -83,6 +94,8 @@ Proof.
unfold RangeValidatorCmd in ranges_valid.
destruct (validIntervalboundsCmd f A P dVars) eqn:iv_valid.
- eapply validIntervalboundsCmd_sound; eauto.
- discriminate.
(*
- pose (iexpmap := (FloverMap.empty (affine_form Q))).
pose (inoise := 1%nat).
epose (imap := (fun _ : nat => None)).
......@@ -104,4 +117,5 @@ Proof.
exprAfs noise iexpmap inoise imap
Hchecked Hinoise Himap Hafcheck H H1 H3 HfVars)
as [map2 [af [vR [aiv [aerr sound_affine]]]]]; intuition.
*)
Qed.
\ No newline at end of file
coq/SMTArith.v
View file @ aca4ef84
......@@ -257,7 +257,7 @@ Definition eval_precond E (P: FloverMap.t intv) :=
-> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
*)
(* TODO: move eval_precond and eqb_var somewhere else *)
(* TODO: move eqb_var, find_in_precond and eval_precond and somewhere else *)
Lemma eqb_var x e : FloverMapFacts.P.F.eqb (Var Q x) e = true -> e = Var Q x.
Proof.
rewrite eqb_cmp_eq. destruct e; cbn; try discriminate.
......@@ -274,9 +274,10 @@ Proof.
apply eqb_var in Heq. cbn in *. now subst.
Qed.
Definition eval_precond E (P: FloverMap.t intv) :=
forall x iv, List.In (Var Q x, iv) (FloverMap.elements P)
-> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
Definition eval_precond fVars E (P: FloverMap.t intv) :=
forall x iv, (x ∈ fVars) ->
List.In (Var Q x, iv) (FloverMap.elements P) ->
exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
Definition addVarConstraint (el: expr Q * intv) q :=
match el with
......@@ -287,21 +288,23 @@ Definition addVarConstraint (el: expr Q * intv) q :=
Definition precond2SMT (P: FloverMap.t intv) :=
List.fold_right addVarConstraint TrueQ (FloverMap.elements P).
Lemma pre_to_smt_correct E P :
eval_precond E P -> eval_smt_logic E (precond2SMT P).
Lemma pre_to_smt_correct fVars E P :
eval_precond fVars E P -> eval_smt_logic E (precond2SMT P).
Proof.
unfold eval_precond, precond2SMT.
induction (FloverMap.elements P) as [|[e [lo hi]] l IHl].
- intros. cbn. auto.
- intros. now cbn.
- intros H. cbn.
destruct e; try (apply IHl; intros x iv inl; apply H; cbn; auto).
destruct e; try (apply IHl; intros x iv infv inl; apply H; cbn; auto).
repeat split.
+ destruct (H n (lo, hi)) as [v [? ?]]; cbn; auto.
admit.
exists (Q2R lo), v. repeat split; try now constructor. tauto.
+ destruct (H n (lo, hi)) as [v H']; cbn; auto.
exists (Q2R lo), v. repeat split. 3: tauto. 1-2: constructor. tauto.
+ destruct (H n (lo, hi)) as [v H']; cbn; auto.
exists v, (Q2R hi). repeat split. 3: tauto. 1-2: constructor. tauto.
+ apply IHl. intros x iv inl. apply H; cbn; auto.
Qed.
admit.
exists v, (Q2R hi). repeat split; try now constructor. tauto.
+ apply IHl. intros x iv infv inl. apply H; cbn; auto.
Abort.
(*
Lemma smt_to_pre_correct E P :
......@@ -400,17 +403,20 @@ Proof.
Qed.
*)
Lemma checkPre_pre_smt E P q :
checkPre P q = true -> eval_precond E P -> eval_smt_logic E q.
Lemma checkPre_pre_smt fVars E P q :
checkPre P q = true ->
NatSet.Subset (varsLogic q) fVars ->
eval_precond fVars E P ->
eval_smt_logic E q.
Proof with try discriminate.
unfold checkPre, eval_precond.
induction (FloverMap.elements P) as [|[e [lo hi]] l IHl] in q |- *.
- destruct q; cbn; intros chk... now auto.
- destruct e as [x| | | | |].
all: cbn; try (intros H0 H1; apply IHl; auto; intros e' x iv Hin Heq;
apply (H1 e'); auto).
all: cbn; try (intros H0 H1 H2; apply IHl; auto; intros e' x iv Hin Heq;
apply (H2 e'); auto).
destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
intros chk H.
intros chk sub H.
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [r| | | | | |]... destruct e2 as [|y| | | | |]...
destruct q2 as [? ?|? ?|? ?| |?|q1 q2|? ?]...
......@@ -424,12 +430,13 @@ Proof with try discriminate.
apply Qeq_bool_eq in chk2. apply Qeq_bool_eq in chk1.
rewrite <- chk3, <- chk4.
apply Qeq_sym in chk2. apply Qeq_sym in chk1.
assert (x ∈ fVars) as fx by (subst; set_tac; set_tac).
repeat split.
+ destruct (H x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
exists (Q2R r), v. repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
+ destruct (H x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
exists v, (Q2R r'). repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
+ apply IHl; auto.
+ apply IHl; auto. set_tac. set_tac.
Qed.
(*
......@@ -469,25 +476,27 @@ Proof with try discriminate.
Qed.
*)
Lemma precond_bound_correct E P preQ bound :
eval_precond E P
Lemma precond_bound_correct fVars E P preQ bound :
eval_precond fVars E P
-> NatSet.Subset (varsLogic preQ) fVars
-> checkPre P preQ = true
-> eval_smt_logic E bound
-> eval_smt_logic E (AndQ preQ bound).
Proof.
intros H1 H2 H3.
intros.
split; auto.
eapply checkPre_pre_smt; eauto.
Qed.
Lemma RangeBound_low_sound E P preQ e r Gamma v :
eval_precond E P
Lemma RangeBound_low_sound fVars E P preQ e r Gamma v :
eval_precond fVars E P
-> NatSet.Subset (varsLogic preQ) fVars
-> checkPre P preQ = true
-> ~ eval_smt_logic E (AndQ preQ (AndQ (LessQ e (ConstQ r)) TrueQ))
-> eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL
-> Q2R r <= v.
Proof.
intros H1 H2 H3 H4.
intros H0 H1 H2 H3 H4.
apply eval_expr_smt in H4.
apply Rnot_lt_le. intros B.
apply H3. eapply precond_bound_correct; eauto.
......@@ -495,14 +504,15 @@ Proof.
do 2 eexists. repeat split; first [eassumption | constructor].
Qed.
Lemma RangeBound_high_sound E P preQ e r Gamma v :
eval_precond E P
Lemma RangeBound_high_sound fVars E P preQ e r Gamma v :
eval_precond fVars E P
-> NatSet.Subset (varsLogic preQ) fVars
-> checkPre P preQ = true
-> ~ eval_smt_logic E (AndQ preQ (AndQ (LessQ (ConstQ r) e) TrueQ))
-> eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL
-> v <= Q2R r.
Proof.
intros H1 H2 H3 H4.
intros H0 H1 H2 H3 H4.
apply eval_expr_smt in H4.
apply Rnot_lt_le. intros B.
apply H3. eapply precond_bound_correct; eauto.
......
coq/SMTValidation.v
View file @ aca4ef84
......@@ -34,15 +34,8 @@ Definition tightenBounds (e: expr Q) (iv: intv) (qMap: FloverMap.t (SMTLogic * S
| Some (loQ, hiQ) => (tightenLowerBound e (fst iv) loQ P, tightenUpperBound e (snd iv) hiQ P)
end.
(* TODO: debug this ltac *)
Ltac query_simpl :=
match goal with
| [ |- context[match ?q with | _ => _ end ]] => fail; destruct q; query_simpl
| _ => idtac
end.
Lemma tightenBounds_low_sound E Gamma e v iv qMap P :
eval_precond E P
Lemma tightenBounds_low_sound fVars E Gamma e v iv qMap P :
eval_precond fVars E P
-> (forall ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E ql)
-> eval_expr E (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) v REAL
-> (Q2R (fst iv) <= v)%R
......@@ -64,12 +57,15 @@ Proof.
rewrite <- Q2R_max. apply Rmax_lub; auto.
eapply RangeBound_low_sound; eauto.
erewrite eval_smt_expr_complete in H; eauto.
(*
rewrite SMTArith2Expr_exact.
exact H.
Qed.
*)
Admitted.
Lemma tightenBounds_high_sound E Gamma e v iv qMap P :
eval_precond E P
Lemma tightenBounds_high_sound fVars E Gamma e v iv qMap P :
eval_precond fVars E P
-> (forall ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E qh)
-> eval_expr E (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) v REAL
-> (v <= Q2R (snd iv))%R
......@@ -90,13 +86,16 @@ Proof.
andb_to_prop Hchk.
rewrite <- Q2R_min. apply Rmin_glb; auto.
eapply RangeBound_high_sound; eauto.
(*
erewrite eval_smt_expr_complete in H; eauto.
rewrite SMTArith2Expr_exact.
exact H.
Qed.
*)
Admitted.
Lemma tightenBounds_sound E Gamma e v iv qMap P :
eval_precond E P
Lemma tightenBounds_sound fVars E Gamma e v iv qMap P :
eval_precond fVars E P
-> (forall ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E ql /\ ~ eval_smt_logic E qh)
-> eval_expr E (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) v REAL
-> (Q2R (fst iv) <= v <= Q2R (snd iv))%R
......@@ -109,6 +108,7 @@ Proof.
intros. edestruct unsatQ; eauto.
Qed.
(* TODO: move this somewher else *)
Lemma Rle_trans2 a b x y z :
(a <= x)%R -> (z <= b)%R -> (x <= y <= z)%R -> (a <= y <= b)%R.
Proof. lra. Qed.
......@@ -202,16 +202,17 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: FloverMap.t
end.
Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: FloverMap.t intv)
(Q: FloverMap.t (SMTLogic * SMTLogic)) dVars (E: env) Gamma :
(Q: FloverMap.t (SMTLogic * SMTLogic)) fVars dVars (E: env) Gamma :
unsat_queries E Q ->
validSMTIntervalbounds f A P Q dVars = true ->
dVars_range_valid dVars E A ->
eval_precond E P ->
NatSet.Subset ((Expressions.usedVars f) -- dVars) fVars ->
eval_precond fVars E P ->
validTypes f Gamma ->
validRanges f A E (toRTMap (toRExpMap Gamma)).
Proof.
induction f;
intros unsat_qs valid_bounds valid_definedVars valid_precond types_defined;
intros unsat_qs valid_bounds valid_definedVars usedVars_subset valid_precond types_defined;
cbn in *.
- destruct (NatSet.mem n dVars) eqn:?; cbn in *; split; auto.
+ destruct (valid_definedVars n)
......@@ -226,7 +227,7 @@ Proof.
match_simpl; auto.
+ Flover_compute.
destruct (valid_precond n i0) as [vR [env_valid bounds_valid]];
auto using find_in_precond.
auto using find_in_precond; set_tac.
canonize_hyps.
kill_trivial_exists.
eexists; split; [auto | split].
......@@ -291,9 +292,9 @@ Proof.
- destruct types_defined
as [? [? [[? [? ?]]?]]].
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
by (Flover_compute; try congruence; apply IHf1; try auto).
by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
by (Flover_compute; try congruence; apply IHf2; try auto).
by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
repeat split;
[ intros; subst; Flover_compute; congruence |
auto | auto |].
......@@ -371,11 +372,11 @@ Proof.
- destruct types_defined
as [mG [find_mg [[validt_f1 [validt_f2 [validt_f3 valid_join]]] valid_exec]]].
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
by (Flover_compute; try congruence; apply IHf1; try auto).
by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
by (Flover_compute; try congruence; apply IHf2; try auto).
by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
assert (validRanges f3 A E (toRTMap (toRExpMap Gamma))) as valid_f3
by (Flover_compute; try congruence; apply IHf3; try auto).
by (Flover_compute; try congruence; apply IHf3; try auto; set_tac).
repeat split; try auto.
apply validRanges_single in valid_f1;
apply validRanges_single in valid_f2;
......
coq/testcase_aritmetic.v
View file @ aca4ef84
......@@ -79,15 +79,16 @@ Proof.
Qed.
Theorem RangeBound_e2_sound E Gamma v :
eval_precond E thePrecondition_fnc1
eval_precond (usedVars e2) E thePrecondition_fnc1
-> ~ eval_smt_logic E query
-> eval_expr E (toRTMap Gamma) (toREval (toRExp e2)) v REAL
-> v <= Q2R ((8201)#(2048)).
Proof.
intros H1 H2 H3.
rewrite e2_to_smt in H3.
eapply (RangeBound_high_sound (preQ:= prec_reorder) H1 _ _ H3).
eapply (RangeBound_high_sound (preQ:= prec_reorder) H1 _ _ _ H3).
Unshelve.
- set_tac.
- reflexivity.