Skip to content

GitLab

F
FloVer
Commit 858945d3 authored by Joachim Bard's avatar Joachim Bard
Browse files
Options

support for additional conditions in precond

parent 45e4ff7a
Hide whitespace changes
Inline Side-by-side
Showing with 298 additions and 99 deletions
coq/AffineValidation.v
View file @ 858945d3
......@@ -25,7 +25,7 @@ Definition nozeroiv iv :=
((Qleb (ivhi iv) 0) && (negb (Qeq_bool (ivhi iv) 0))) ||
((Qleb 0 (ivlo iv)) && (negb (Qeq_bool (ivlo iv) 0))).
Fixpoint validAffineBounds (e: expr Q) (A: analysisResult) (P: precond) (validVars: NatSet.t)
Fixpoint validAffineBounds (e: expr Q) (A: analysisResult) P (validVars: NatSet.t)
(exprsAf: expressionsAffine) (currentMaxNoise: nat): option (expressionsAffine * nat) :=
match FloverMap.find e exprsAf with
| Some _ =>
......@@ -688,7 +688,7 @@ Lemma validAffineBounds_sound_var A P E Gamma fVars dVars n:
validAffineBounds (Var Q n) A P dVars iexpmap inoise = Some (exprAfs, noise) ->
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars (Var Q n) -- dVars) fVars ->
eval_precond E P ->
P_intv_sound E P ->
validTypes (Var Q n) Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error),
......@@ -885,7 +885,7 @@ Lemma validAffineBounds_sound_const A P E Gamma fVars dVars m v:
validAffineBounds (Const m v) A P dVars iexpmap inoise = Some (exprAfs, noise) ->
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars (Const m v) -- dVars) fVars ->
eval_precond E P ->
P_intv_sound E P ->
validTypes (Const m v) Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error),
......@@ -1009,7 +1009,7 @@ Definition validAffineBounds_IH_e A P E Gamma fVars dVars e :=
validAffineBounds e A P dVars iexpmap inoise = Some (exprAfs, noise) ->
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars e -- dVars) fVars ->
eval_precond E P ->
P_intv_sound E P ->
validTypes e Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error),
......@@ -1041,7 +1041,7 @@ Lemma validAffineBounds_sound_unop A P E Gamma fVars dVars u e:
validAffineBounds (Unop u e) A P dVars iexpmap inoise = Some (exprAfs, noise) ->
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars (Unop u e) -- dVars) fVars ->
eval_precond E P ->
P_intv_sound E P ->
validTypes (Unop u e) Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error),
......@@ -1232,7 +1232,7 @@ Lemma validAffineBounds_sound_binop A P E Gamma fVars dVars b e1 e2:
validAffineBounds (Binop b e1 e2) A P dVars iexpmap inoise = Some (exprAfs, noise) ->
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars (Binop b e1 e2) -- dVars) fVars ->
eval_precond E P ->
P_intv_sound E P ->
validTypes (Binop b e1 e2) Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error),
......@@ -1808,7 +1808,7 @@ Lemma validAffineBounds_sound_fma A P E Gamma fVars dVars e1 e2 e3:
validAffineBounds (Fma e1 e2 e3) A P dVars iexpmap inoise = Some (exprAfs, noise) ->
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars (Fma e1 e2 e3) -- dVars) fVars ->
eval_precond E P ->
P_intv_sound E P ->
validTypes (Fma e1 e2 e3) Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error),
......@@ -2097,7 +2097,7 @@ Lemma validAffineBounds_sound_downcast A P E Gamma fVars dVars m e:
validAffineBounds (Downcast m e) A P dVars iexpmap inoise = Some (exprAfs, noise) ->
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars (Downcast m e) -- dVars) fVars ->
eval_precond E P ->
P_intv_sound E P ->
validTypes (Downcast m e) Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error),
......@@ -2197,7 +2197,7 @@ Proof.
apply visitedSubexpr; eauto.
Qed.
Lemma validAffineBounds_sound (e: expr Q) (A: analysisResult) (P: precond)
Lemma validAffineBounds_sound (e: expr Q) (A: analysisResult) P
fVars dVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
(forall e, (exists af, FloverMap.find e iexpmap = Some af) ->
checked_expressions A E Gamma fVars dVars e iexpmap inoise map1) ->
......@@ -2206,7 +2206,7 @@ Lemma validAffineBounds_sound (e: expr Q) (A: analysisResult) (P: precond)
validAffineBounds e A P dVars iexpmap inoise = Some (exprAfs, noise) ->
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
eval_precond E P ->
P_intv_sound E P ->
validTypes e Gamma ->
exists map2 af vR aiv aerr,
contained_map map1 map2 /\
......@@ -2230,7 +2230,7 @@ Proof.
validAffineBounds_sound_fma, validAffineBounds_sound_downcast.
Qed.
Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (validVars: NatSet.t)
Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) P (validVars: NatSet.t)
(exprsAf: expressionsAffine) (currentMaxNoise: nat): option (expressionsAffine * nat) :=
match c with
| Let m x e c' => match FloverMap.find e A, FloverMap.find (Var Q x) A with
......@@ -2250,7 +2250,7 @@ Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (valid
| Ret e => validAffineBounds e A P validVars exprsAf currentMaxNoise
end.
Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond)
Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) P
fVars dVars outVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
(forall e, (exists af, FloverMap.find e iexpmap = Some af) ->
checked_expressions A E Gamma fVars dVars e iexpmap inoise map1) ->
......@@ -2260,8 +2260,8 @@ Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond)
ssa c (NatSet.union fVars dVars) outVars ->
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (NatSet.diff (Commands.freeVars c) dVars) fVars ->
NatSet.Subset (preVars P) fVars ->
eval_precond E P ->
NatSet.Subset (preIntvVars P) fVars ->
P_intv_sound E P ->
validTypesCmd c Gamma ->
exists map2 af vR aiv aerr,
contained_map map1 map2 /\
......@@ -2387,7 +2387,7 @@ Proof.
apply a_no_dVar.
rewrite NatSet.add_spec; auto. }
}
assert (eval_precond (updEnv n vR E) P) as H4'''.
assert (P_intv_sound (updEnv n vR E) P) as H4'''.
{
intros v0 iv inP.
unfold updEnv.
......@@ -2395,7 +2395,7 @@ Proof.
rewrite Nat.eqb_eq in case_v0; subst.
exfalso; set_tac. apply H6.
apply NatSetProps.union_subset_1. apply varsP_free.
exact (preVars_sound _ _ _ inP).
exact (preIntvVars_sound _ _ _ inP).
}
edestruct IHc with (E := updEnv n vR E) (Gamma := Gamma)
(dVars := NatSet.add n dVars)
......
coq/CertificateChecker.v
View file @ 858945d3
......@@ -13,7 +13,7 @@ Require Export ExpressionSemantics Flover.Commands Coq.QArith.QArith Flover.SMTA
(** Certificate checking function **)
Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
(P:FloverMap.t intv) Qmap (defVars:FloverMap.t mType):=
(P: precond) Qmap (defVars:FloverMap.t mType):=
let tMap := (getValidMap defVars e (FloverMap.empty mType)) in
match tMap with
|Succes tMap =>
......@@ -88,7 +88,7 @@ Proof.
exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto.
Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: FloverMap.t intv)
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: precond)
(Qmap: FloverMap.t (SMTLogic * SMTLogic)) defVars :=
match getValidMapCmd defVars f (FloverMap.empty mType) with
| Succes Gamma =>
......
coq/Checker_extraction.v
View file @ 858945d3
......@@ -3,4 +3,4 @@ Require Import Coq.extraction.ExtrOcamlString Coq.extraction.ExtrOcamlBasic Coq.
Extraction Language Ocaml.
Extraction "./binary/CoqChecker.ml" runChecker.
\ No newline at end of file
Extraction "./binary/CoqChecker.ml" runChecker.
coq/Environments.v
View file @ 858945d3
......@@ -153,4 +153,4 @@ Section RelationProperties.
* apply IHa; auto.
Qed.
End RelationProperties.
\ No newline at end of file
End RelationProperties.
coq/IEEE_connection.v
View file @ 858945d3
......@@ -1140,7 +1140,7 @@ Theorem IEEE_connection_expr e A P qMap E1 E2 defVars DeltaMap:
noDowncast (B2Qexpr e) ->
eval_expr_valid e E2 ->
unsat_queries qMap ->
eval_precond E1 P ->
P_intv_sound E1 P ->
CertificateChecker (B2Qexpr e) A P qMap defVars = true ->
exists Gamma, (* m, currently = M64 *)
approxEnv E1 Gamma A (usedVars (B2Qexpr e)) (NatSet.empty) (toREnv E2) ->
......@@ -1210,7 +1210,7 @@ Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P qMap
noDowncastFun (B2Qcmd f) ->
bstep_valid f E2 ->
unsat_queries qMap ->
eval_precond E1 P ->
P_intv_sound E1 P ->
CertificateCheckerCmd (B2Qcmd f) A P qMap defVars = true ->
exists Gamma,
approxEnv E1 (toRExpMap Gamma) A (freeVars (B2Qcmd f)) NatSet.empty (toREnv E2) ->
......
coq/Infra/ExpressionAbbrevs.v
View file @ 858945d3
......@@ -182,7 +182,7 @@ Definition expressionsAffine: Type := FloverMap.t (affine_form Q).
Later we will argue about program preconditions.
Define a precondition to be a function mapping numbers (resp. variables) to intervals.
**)
Definition precond : Type := FloverMap.t intv.
Definition precondIntv : Type := FloverMap.t intv.
Definition contained_flover_map V expmap1 expmap2 :=
forall (e: expr Q) (v: V), FloverMap.find e expmap1 = Some v -> FloverMap.find e expmap2 = Some v.
......
coq/IntervalValidation.v
View file @ 858945d3
......@@ -148,7 +148,7 @@ Theorem validIntervalbounds_sound (f:expr Q) (A:analysisResult) (P: FloverMap.t
validIntervalbounds f A P dVars = true ->
dVars_range_valid dVars E A ->
NatSet.Subset ((Expressions.usedVars f) -- dVars) fVars ->
eval_precond E P ->
P_intv_sound E P ->
validTypes f Gamma ->
validRanges f A E (toRTMap (toRExpMap Gamma)).
Proof.
......@@ -392,15 +392,15 @@ 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 (preVars P) fVars ->
P_intv_sound E P ->
NatSet.Subset (preIntvVars P) fVars ->
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 preVars_free usedVars_subset
intros * ssa_f dVars_sound fVars_valid preIntvVars_free usedVars_subset
valid_bounds_f valid_types_f;
cbn in *.
- Flover_compute.
......@@ -445,7 +445,7 @@ Proof.
rewrite Nat.eqb_eq in case_x. subst.
set_tac.
assert (NatSet.In n fVars) as in_free
by (apply preVars_free; eapply preVars_sound; eauto).
by (apply preIntvVars_free; eapply preIntvVars_sound; eauto).
(* by (destruct (fVars_valid n iv); auto; set_tac). *)
exfalso. apply H6. set_tac.
- intros x x_contained.
......
coq/RealRangeArith.v
View file @ 858945d3
......@@ -23,12 +23,12 @@ Proof.
Qed.
(*
Definition eval_precond E (P: precond) :=
Definition P_intv_sound E (P: precond) :=
forall x iv, FloverMap.find (Var Q x) P = Some iv
-> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
*)
Definition eval_precond E (P: precond) :=
Definition P_intv_sound E (P: precondIntv) :=
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))%R.
......@@ -38,13 +38,13 @@ Definition addVar2Set (elt: (expr Q * intv)) s :=
| _ => s
end.
Definition preVars (P: precond) :=
Definition preIntvVars (P: precondIntv) :=
List.fold_right addVar2Set NatSet.empty (FloverMap.elements P).
Lemma preVars_sound P x iv :
List.In (Var Q x, iv) (FloverMap.elements P) -> x ∈ (preVars P).
Lemma preIntvVars_sound P x iv :
List.In (Var Q x, iv) (FloverMap.elements P) -> x ∈ (preIntvVars P).
Proof.
unfold preVars.
unfold preIntvVars.
induction (FloverMap.elements P).
- cbn. tauto.
- cbn. intros [-> | ?]; cbn; set_tac.
......
coq/RealRangeValidator.v
View file @ 858945d3
......@@ -13,9 +13,9 @@ From Flover
Definition RangeValidator e A P Qmap dVars :=
if
validIntervalbounds e A P dVars
validIntervalbounds e A (fst P) dVars
then true
else match validAffineBounds e A P dVars (FloverMap.empty (affine_form Q)) 1 with
else match validAffineBounds e A (fst P) dVars (FloverMap.empty (affine_form Q)) 1 with
| Some _ => true
| None => validSMTIntervalbounds e A P Qmap (fun _ => None) dVars
end.
......@@ -32,15 +32,18 @@ Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : precond)
Proof.
intros.
unfold RangeValidator in *.
destruct (validIntervalbounds e A P dVars) eqn: Hivcheck.
destruct P as [Piv C].
destruct (validIntervalbounds e A Piv dVars) eqn: Hivcheck.
- eapply validIntervalbounds_sound; set_tac; eauto.
unfold eval_precond in *. tauto.
(* unfold dVars_range_valid; intros; set_tac. *)
- 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 now (eapply validSMTIntervalbounds_sound; set_tac; eauto).
cbn in H. rewrite Hivcheck in H.
destruct (validAffineBounds e A Piv dVars iexpmap inoise) eqn: Hafcheck.
2: now eapply validSMTIntervalbounds_sound; set_tac; eauto.
clear H.
destruct p as [exprAfs noise].
pose proof (validAffineBounds_sound) as sound_affine.
......@@ -53,8 +56,8 @@ 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.
rename H3 into Hpre.
specialize (sound_affine e A P (usedVars e) dVars E Gamma
destruct H3 as [Hpre _].
specialize (sound_affine e A Piv (usedVars e) dVars E Gamma
exprAfs noise iexpmap inoise imap
Hchecked Hinoise Himap Hafcheck H1 Hsubset Hpre)
as [map2 [af [vR [aiv [aerr sound_affine]]]]]; intuition.
......@@ -62,9 +65,9 @@ Qed.
Definition RangeValidatorCmd e A P Qmap dVars:=
if
validIntervalboundsCmd e A P dVars
validIntervalboundsCmd e A (fst P) dVars
then true
else match validAffineBoundsCmd e A P dVars (FloverMap.empty (affine_form Q)) 1 with
else match validAffineBoundsCmd e A (fst P) dVars (FloverMap.empty (affine_form Q)) 1 with
| Some _ => true
| None => validSMTIntervalboundsCmd e A P Qmap (fun _ => None) dVars
end.
......@@ -85,14 +88,19 @@ Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond)
Proof.
intros ranges_valid; intros.
unfold RangeValidatorCmd in ranges_valid.
destruct (validIntervalboundsCmd f A P dVars) eqn:iv_valid.
destruct P as [Piv C].
destruct (validIntervalboundsCmd f A Piv dVars) eqn:iv_valid.
- eapply validIntervalboundsCmd_sound; eauto.
+ unfold eval_precond in *. tauto.
+ unfold preVars in *. eapply NatSetProps.subset_trans.
apply NatSetProps.union_subset_1. 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 now (eapply validSMTIntervalboundsCmd_sound; eauto).
cbn in ranges_valid. rewrite iv_valid in ranges_valid.
destruct (validAffineBoundsCmd f A Piv dVars iexpmap inoise) eqn: Hafcheck.
2: now (eapply validSMTIntervalboundsCmd_sound; eauto).
destruct p as [exprAfs noise].
pose proof (validAffineBoundsCmd_sound) as sound_affine.
assert ((forall e' : FloverMap.key,
......@@ -103,8 +111,11 @@ Proof.
congruence).
assert (1 > 0)%nat as Hinoise by omega.
eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
specialize (sound_affine f A P fVars dVars outVars E Gamma
specialize (sound_affine f A Piv fVars dVars outVars E Gamma
exprAfs noise iexpmap inoise imap
Hchecked Hinoise Himap Hafcheck H H1 H4 H3 H2)
Hchecked Hinoise Himap Hafcheck H H1 H4)
as [map2 [af [vR [aiv [aerr sound_affine]]]]]; intuition.
+ unfold preVars in *. eapply NatSetProps.subset_trans.
apply NatSetProps.union_subset_1. eauto.
+ unfold eval_precond in *. tauto.
Qed.
coq/SMTArith.v
View file @ 858945d3
......@@ -33,8 +33,6 @@ Inductive SMTLogic :=
Definition FalseQ := NotQ TrueQ.
Definition usedQueries : Type := FloverMap.t (SMTLogic * SMTLogic).
Definition getPrecond q :=
match q with
| AndQ p _ => Some p
......@@ -82,6 +80,30 @@ Proof. cbn. tauto. Qed.
Lemma not_eval_falseq E : ~ eval_smt_logic E FalseQ.
Proof. auto. Qed.
Fixpoint SMTArith_eqb e e' : bool :=
match e, e' with
| ConstQ r, ConstQ r' => Qeq_bool r r'
| VarQ x, VarQ x' => beq_nat x x'
| UMinusQ e, UMinusQ e' => SMTArith_eqb e e'
| PlusQ e1 e2, PlusQ e1' e2' => SMTArith_eqb e1 e1' && SMTArith_eqb e2 e2'
| MinusQ e1 e2, MinusQ e1' e2' => SMTArith_eqb e1 e1' && SMTArith_eqb e2 e2'
| TimesQ e1 e2, TimesQ e1' e2' => SMTArith_eqb e1 e1' && SMTArith_eqb e2 e2'
| DivQ e1 e2, DivQ e1' e2' => SMTArith_eqb e1 e1' && SMTArith_eqb e2 e2'
| _, _ => false
end.
Fixpoint SMTLogic_eqb q q' : bool :=
match q, q' with
| LessQ q1 q2, LessQ q1' q2' => SMTArith_eqb q1 q1' && SMTArith_eqb q2 q2'
| LessEqQ q1 q2, LessEqQ q1' q2' => SMTArith_eqb q1 q1' && SMTArith_eqb q2 q2'
| EqualsQ q1 q2, EqualsQ q1' q2' => SMTArith_eqb q1 q1' && SMTArith_eqb q2 q2'
| TrueQ, TrueQ => true
| NotQ q, NotQ q' => SMTLogic_eqb q q'
| AndQ q1 q2, AndQ q1' q2' => SMTLogic_eqb q1 q1' && SMTLogic_eqb q2 q2'
| OrQ q1 q2, OrQ q1' q2' => SMTLogic_eqb q1 q1' && SMTLogic_eqb q2 q2'
| _, _ => false
end.
Fixpoint SMTArith2Expr (e: SMTArith) : expr Q :=
match e with
| ConstQ r => Expressions.Const REAL r
......@@ -93,6 +115,70 @@ Fixpoint SMTArith2Expr (e: SMTArith) : expr Q :=
| DivQ e1 e2 => Binop Div (SMTArith2Expr e1) (SMTArith2Expr e2)
end.
Lemma SMTArith_eqb_refl e : SMTArith_eqb e e = true.
Proof.
induction e; cbn; try rewrite IHe1, IHe2; auto using Qeq_bool_refl, Nat.eqb_refl.
Qed.
Lemma SMTLogic_eqb_refl q : SMTLogic_eqb q q = true.
Proof.
induction q; cbn; try rewrite IHq1, IHq2; auto; now rewrite ?SMTArith_eqb_refl.
Qed.
Lemma SMTArith_eqb_sym e e' : SMTArith_eqb e e' = SMTArith_eqb e' e.
Proof.
induction e in e' |- *; destruct e'; cbn; auto using Qeq_bool_comm, Nat.eqb_sym;
try (rewrite IHe1, IHe2; reflexivity).
Qed.
Lemma SMTArith_eqb_sound E e e' v :
SMTArith_eqb e e' = true ->
eval_smt E e v ->
eval_smt E e' v.
Proof.
induction e in e', v |- *; destruct e'; cbn; try discriminate.
- intros Heq H. inversion H; subst. apply Qeq_bool_eq, Qeq_eqR in Heq.
rewrite Heq. constructor.
- intros Heq H. apply beq_nat_true in Heq. inversion H; subst.
now constructor.
- intros Heq H. inversion H; subst. constructor. auto.
- intros Heq H. andb_to_prop Heq. inversion H; subst.
constructor; auto.
- intros Heq H. andb_to_prop Heq. inversion H; subst.
constructor; auto.
- intros Heq H. andb_to_prop Heq. inversion H; subst.
constructor; auto.
- intros Heq H. andb_to_prop Heq. inversion H; subst.
constructor; auto.
Qed.
Lemma SMTLogic_eqb_sound E q q' :
SMTLogic_eqb q q' = true ->
eval_smt_logic E q <-> eval_smt_logic E q'.
Proof.
induction q in q' |- *; destruct q'; cbn; try discriminate.
- intros H. andb_to_prop H.
split; intros [v1 [v2 [H1 [H2 H3]]]]; exists v1, v2; repeat split;
eauto using SMTArith_eqb_sound.
all: rewrite SMTArith_eqb_sym in L, R; eauto using SMTArith_eqb_sound.
- intros H. andb_to_prop H.
split; intros [v1 [v2 [H1 [H2 H3]]]]; exists v1, v2; repeat split;
eauto using SMTArith_eqb_sound.
all: rewrite SMTArith_eqb_sym in L, R; eauto using SMTArith_eqb_sound.
- intros H. andb_to_prop H.
split; intros [v [H1 H2]]; exists v; repeat split;
eauto using SMTArith_eqb_sound.
all: rewrite SMTArith_eqb_sym in L, R; eauto using SMTArith_eqb_sound.
- tauto.
- intros Heq. split; intros nH H; now apply nH, (IHq q').
- intros H. andb_to_prop H. split; intros [H1 H2]; split.
all: try now apply (IHq1 _ L).
all: now apply (IHq2 _ R).
- intros H. andb_to_prop H. split; intros [H1 | H2].
all: try (left; now apply (IHq1 _ L)).
all: right; now apply (IHq2 _ R).
Qed.
Lemma SMTArith2Expr_exact e : toREval (toRExp (SMTArith2Expr e)) = toRExp (SMTArith2Expr e).
Proof.
induction e; cbn; auto; now rewrite ?IHe, ?IHe1, ?IHe2.
......@@ -236,8 +322,91 @@ Fixpoint varsLogic (q: SMTLogic) :=
| OrQ q1 q2 => varsLogic q1 ∪ varsLogic q2
end.
Lemma eval_smt_updEnv x v r E e :
~ (x ∈ varsSMT e) ->
eval_smt E e v <-> eval_smt (updEnv x r E) e v.
Proof.
induction e in v |- *; intros Hx.
- split; intros H; inversion H; subst; constructor.
- split; intros H; inversion H; subst; constructor.
+ unfold updEnv. cbn in Hx. case_eq (x0 =? x); auto.
intros Heq. exfalso. apply Hx. set_tac. symmetry. now apply beq_nat_true.
+ unfold updEnv in *. cbn in Hx. case_eq (x0 =? x); intros Heq; rewrite Heq in *; auto.
exfalso. apply Hx. set_tac. symmetry. now apply beq_nat_true.
- split; intros H; inversion H; subst; constructor; apply IHe; auto.
- split; intros H; inversion H; subst; constructor.
all: try apply IHe1; auto.
all: try apply IHe2; auto.
all: intros ?; apply Hx; cbn; set_tac.
- split; intros H; inversion H; subst; constructor.
all: try apply IHe1; auto.
all: try apply IHe2; auto.
all: intros ?; apply Hx; cbn; set_tac.
- split; intros H; inversion H; subst; constructor.
all: try apply IHe1; auto.
all: try apply IHe2; auto.
all: intros ?; apply Hx; cbn; set_tac.
- split; intros H; inversion H; subst; constructor.
all: try apply IHe1; auto.
all: try apply IHe2; auto.
all: intros ?; apply Hx; cbn; set_tac.
Qed.
Lemma eval_smt_logic_updEnv x v E q :
~ (x ∈ varsLogic q) ->
eval_smt_logic E q <-> eval_smt_logic (updEnv x v E) q.
Proof.
intros H. induction q; cbn.
- split; intros [v1 [v2 [H1 [H2 H3]]]]; exists v1, v2; repeat split; auto.
all: try apply eval_smt_updEnv; auto.
all: try eapply eval_smt_updEnv; eauto.
all: try (intros ?; apply H; cbn; set_tac).
- split; intros [v1 [v2 [H1 [H2 H3]]]]; exists v1, v2; repeat split; auto.
all: try apply eval_smt_updEnv; auto.
all: try eapply eval_smt_updEnv; eauto.
all: try (intros ?; apply H; cbn; set_tac).
- split; intros [v' [H1 H2]]; exists v'; repeat split; auto.
all: try apply eval_smt_updEnv; auto.
all: try eapply eval_smt_updEnv; eauto.
all: try (intros ?; apply H; cbn; set_tac).
- tauto.
- split; intros H1 H2; apply H1; apply IHq; auto.
- split; intros [H1 H2]; split.
all: try apply IHq1; auto.
all: try apply IHq2; auto.
all: intros Hx; apply H; cbn; set_tac.
- split; (intros [H1 | H2]; [left | right]).
all: try apply IHq1; auto.
all: try apply IHq2; auto.
all: intros Hx; apply H; cbn; set_tac.
Qed.
Definition precond : Type := precondIntv * SMTLogic.
Definition preVars (P: precond) := preIntvVars (fst P) ∪ varsLogic (snd P).
Definition eval_precond E (P: precond) :=
P_intv_sound E (fst P) /\ eval_smt_logic E (snd P).
Lemma eval_precond_updEnv E x v P :
eval_precond E P ->
~ (x ∈ preVars P) ->
eval_precond (updEnv x v E) P.
Proof.
unfold preVars. destruct P as [Piv C]. cbn. intros [HPiv HC] H. split.
- unfold P_intv_sound in *.
intros y iv inl. destruct (HPiv y iv) as [r [H1 H2]]; auto.
exists r. split; auto. unfold updEnv. case_eq (y =? x); intros Heq; auto.
exfalso. apply H. set_tac. left. apply beq_nat_true in Heq. subst.
eapply preIntvVars_sound. eauto.
- apply eval_smt_logic_updEnv; auto. intros ?. apply H. set_tac.
Qed.
Definition usedQueries : Type := FloverMap.t (SMTLogic * SMTLogic).
Definition unsat_queries qMap :=
forall E e ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E ql /\ ~ eval_smt_logic E qh.
forall E e ql qh, FloverMap.find e qMap = Some (ql, qh) ->
~ eval_smt_logic E ql /\ ~ eval_smt_logic E qh.
Definition addVarConstraint (el: expr Q * intv) q :=
match el with
......@@ -246,31 +415,33 @@ Definition addVarConstraint (el: expr Q * intv) q :=
end.
Definition precond2SMT (P: precond) :=
List.fold_right addVarConstraint TrueQ (FloverMap.elements P).
List.fold_right addVarConstraint (snd P) (FloverMap.elements (fst P)).
Lemma pre_to_smt_correct E P :
eval_precond E P -> eval_smt_logic E (precond2SMT P).
Proof.
unfold eval_precond, precond2SMT.
induction (FloverMap.elements P) as [|[e [lo hi]] l IHl].
unfold eval_precond, P_intv_sound, precond2SMT.
destruct P as [intvs q]. cbn.
induction (FloverMap.elements intvs) as [|[e [lo hi]] l IHl].
- intros. now cbn.
- intros H. cbn.
destruct e; try (apply IHl; intros x iv inl; apply H; cbn; auto).
- intros [H Hq]. cbn.
destruct e; try (apply IHl; split; auto; intros x iv inl; apply H; cbn; auto).
repeat split.
+ destruct (H n (lo, hi)) as [v [? ?]]; cbn; auto.
exists (Q2R lo), v. repeat split; try now constructor. tauto.
+ destruct (H n (lo, hi)) as [v [? ?]]; cbn; auto.
exists v, (Q2R hi). repeat split; try now constructor. tauto.
+ apply IHl. intros x iv inl. apply H; cbn; auto.
+ apply IHl. split; auto. intros x iv inl. apply H; cbn; auto.
Qed.
Lemma smt_to_pre_correct E P :
eval_smt_logic E (precond2SMT P) -> eval_precond E P.
Proof.
unfold precond2SMT, eval_precond.
induction (FloverMap.elements P) as [|? l IHl].
- cbn. tauto.
- cbn. intros H x [lo hi] [hd | inl].
unfold precond2SMT, eval_precond, P_intv_sound.
destruct P as [intvs q]. cbn.
induction (FloverMap.elements intvs) as [|p l IHl]; try (cbn; tauto).
cbn. intros H. split.
- intros x [lo hi] [hd | inl].
+ subst. cbn in H. destruct H as [H1 [H2 H3]].
destruct H1 as [v1 [v2 H1]].
exists v2. repeat split; destruct H1 as [lov1 [xv2 leq]].
......@@ -279,22 +450,24 @@ Proof.
* destruct H2 as [v1' [v2' [xv1' [hiv2' leq']]]].
inversion xv1'. inversion hiv2'. inversion xv2. subst.
assert (eq: v2 = v1') by congruence. now rewrite eq.
+ apply IHl; auto. destruct a as [e [lo' hi']].