Commit 1974c006 authored by Heiko Becker's avatar Heiko Becker
Browse files

Merge branch 'master' into 'SMT_Subdiv'

Cleanup and adding some comments to final development

See merge request AVA/FloVer!23
parents c40f3832 b6ddcee8
......@@ -11,6 +11,7 @@ compile-coq:
stage: compile
script: ./scripts/ci-coq.sh
artifacts:
expire_in: 1 week
paths:
- coq/
......@@ -18,6 +19,7 @@ compile-hol:
stage: compile
script: ./scripts/ci-hol4.sh
artifacts:
expire_in: 3 weeks
paths:
- hol4/
- HOL4/
......
......@@ -11,6 +11,7 @@ Require Import Flover.RealRangeArith.
Open Scope R.
(* Restricted functions: cast, fma, and let are disallowed *)
Inductive SMTArith :=
| ConstQ (r: Q) : SMTArith
| VarQ (x: nat) : SMTArith
......@@ -20,7 +21,8 @@ Inductive SMTArith :=
| TimesQ (e1 e2: SMTArith) : SMTArith
| DivQ (e1 e2: SMTArith) : SMTArith.
(* SMT of non-linear arithmetic:
comparisons of restricted functions, as well as usual boolean connectives *)
Inductive SMTLogic :=
| LessQ (e1 e2: SMTArith) : SMTLogic
| LessEqQ (e1 e2: SMTArith) : SMTLogic
......@@ -44,6 +46,7 @@ Definition getBound q :=
| _ => None
end.
(* evaluation of restricted functions *)
Inductive eval_smt (E: env) : SMTArith -> R -> Prop :=
| VarQ_load x v : E x = Some v -> eval_smt E (VarQ x) v
| ConstQ_eval r : eval_smt E (ConstQ r) (Q2R r)
......@@ -57,6 +60,7 @@ Inductive eval_smt (E: env) : SMTArith -> R -> Prop :=
| DivQ_eval e1 e2 v1 v2 :
v2 <> 0 -> eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (DivQ e1 e2) (v1 / v2).
(* semantics for SMT-statements *)
Fixpoint eval_smt_logic (E: env) (q: SMTLogic) : Prop :=
match q with
| LessQ e1 e2 => exists v1 v2, eval_smt E e1 v1 /\ eval_smt E e2 v2 /\ v1 < v2
......@@ -183,7 +187,8 @@ Proof.
induction e; cbn; auto; now rewrite ?IHe, ?IHe1, ?IHe2.
Qed.
(* TODO handle Let and Cond *)
(* comparison of functions and restricted functions as given above *)
(* let's are handled separately *)
Fixpoint smt_expr_eq (e: SMTArith) (e': expr Q) : bool :=
match e', e with
| Expressions.Const _ r', ConstQ r => Qeq_bool r r'
......@@ -257,7 +262,6 @@ Proof.
destruct m1; try discriminate.
now apply IHe'.
- cbn. congruence.
(* - cbn. congruence. *)
Qed.
Lemma eval_smt_expr E e v :
......@@ -365,6 +369,7 @@ Proof.
- Flover_compute. erewrite IHq1_1; eauto. erewrite IHq1_2; eauto.
Qed.
(* evaluation only depends on contained variables *)
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.
......@@ -446,6 +451,7 @@ Proof.
- apply eval_smt_logic_updEnv; auto. intros ?. apply H. set_tac.
Qed.
(* define map of SMT-queries and unsatisfiability for them *)
Definition usedQueries : Type := FloverMap.t (SMTLogic * SMTLogic).
Definition unsat_queries qMap :=
......@@ -458,6 +464,7 @@ Definition addVarConstraint (el: expr Q * intv) q :=
| _ => q
end.
(* a precondition can be transformed into and equivalent SMT-statement *)
Definition precond2SMT (P: precond) :=
List.fold_right addVarConstraint (snd P) (FloverMap.elements (fst P)).
......@@ -501,131 +508,32 @@ Proof.
cbn in H. tauto.
Qed.
(* checker for precondition *)
Fixpoint checkPrelist (lP: list (FloverMap.key * intv)) C q : bool :=
match lP, q with
| List.nil, _ => SMTLogic_eqb C q
| List.cons (Var _ x, (lo, hi)) lP', AndQ (LessEqQ (ConstQ lo') (VarQ y)) (AndQ (LessEqQ (VarQ z) (ConstQ hi')) q') => (x =? y) && (x =? z) && Qeq_bool lo lo' && Qeq_bool hi hi' && checkPrelist lP' C q'
| List.cons (Var _ x, _) _, _ => false
| List.cons el lP', _ => checkPrelist lP' C q
end.
(*
Lemma checkPrelist_LessQ lP C e1 e2 : checkPrelist lP C (LessQ e1 e2) = false.
Proof.
induction lP as [|[e [lo hi]] l IHl]; auto.
destruct e; auto.
Qed.
Lemma checkPrelist_LessEqQ lP e1 e2 : checkPrelist lP (LessEqQ e1 e2) = false.
Proof.
induction lP as [|[e [lo hi]] l IHl]; auto.
destruct e; auto.
Qed.
Lemma checkPrelist_EqualsQ lP e1 e2 : checkPrelist lP (EqualsQ e1 e2) = false.
Proof.
induction lP as [|[e [lo hi]] l IHl]; auto.
destruct e; auto.
Qed.
Lemma checkPrelist_NotQ lP q : checkPrelist lP (NotQ q) = false.
Proof.
induction lP as [|[e [lo hi]] l IHl]; auto.
destruct e; auto.
Qed.
Lemma checkPrelist_OrQ lP q1 q2 : checkPrelist lP (OrQ q1 q2) = false.
Proof.
induction lP as [|[e [lo hi]] l IHl]; auto.
destruct e; auto.
Qed.
*)
Definition checkPre (P: precond) q := checkPrelist (FloverMap.elements (fst P)) (snd P) q.
Definition checkPre (P: precond) q := SMTLogic_eqb (precond2SMT P) q.
Lemma checkPre_precond P : checkPre P (precond2SMT P) = true.
Proof.
unfold precond2SMT, checkPre.
destruct P as [Piv C]. cbn.
induction (FloverMap.elements Piv) as [|[e [lo hi]] l IHl]; cbn.
- apply SMTLogic_eqb_refl.
- destruct e; cbn; auto.
now rewrite Nat.eqb_refl, !Qeq_bool_refl, IHl.
unfold checkPre. apply SMTLogic_eqb_refl.
Qed.
Lemma checkPre_pre_smt E P q :
checkPre P q = true ->
eval_precond E P ->
eval_smt_logic E q.
Proof with try discriminate.
unfold checkPre, eval_precond, eval_preIntv.
destruct P as [Piv C]. cbn.
induction (FloverMap.elements Piv) as [|[e [lo hi]] l IHl] in q |- *.
- cbn. intros Heq [_ H]. now apply (SMTLogic_eqb_sound _ C).
- destruct e as [x| | | | | |].
all: try now (cbn; intros Heq [H1 H2]; apply IHl; auto).
cbn.
destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [r| | | | | |]... destruct e2 as [|y| | | | |]...
destruct q2 as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [|z| | | | |]... destruct e2 as [r'| | | | | |]...
intros chk [H HC].
apply andb_prop in chk as [chk chk0].
apply andb_prop in chk as [chk chk1].
apply andb_prop in chk as [chk chk2].
apply andb_prop in chk as [chk4 chk3].
apply beq_nat_true in chk4. apply beq_nat_true in chk3.
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.
Proof.
intros Heq HP.
apply (SMTLogic_eqb_sound _ _ _ Heq).
now apply pre_to_smt_correct.
Qed.
(*
Lemma checkPre_smt_pre E P q :
checkPre P q = true -> eval_smt_logic E q -> eval_precond E P.
Proof with try discriminate.
unfold P_intv_sound, checkPre.
induction (FloverMap.elements P) as [|[e [lo hi]] l IHl] in q |- *.
- destruct q; cbn; intros chk; try discriminate. tauto.
- destruct e as [x| | | | |];
try (intros chk H ? ? [?|?]; [discriminate| apply (IHl _ chk); auto]).
destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [r| | | | | |]... destruct e2 as [|y| | | | |]...
destruct q2 as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [|z| | | | |]... destruct e2 as [r'| | | | | |]...
cbn. intros chk H x' [lo' hi'] [eq|inl].
+ apply andb_prop in chk. destruct chk as [chk chk0].
apply andb_prop in chk. destruct chk as [chk chk1].
apply andb_prop in chk. destruct chk as [chk chk2].
apply andb_prop in chk. destruct chk as [chk4 chk3].
apply beq_nat_true in chk4. apply beq_nat_true in chk3.
apply Qeq_bool_eq in chk2. apply Qeq_bool_eq in chk1.
destruct H as [[v1 [v2 [H1 [H2 H3]]]] [[v1' [v2' [H1' [H2' H3']]]] H]].
symmetry in chk4. symmetry in chk3.
assert (x' = x) by congruence.
assert (lo' = lo) by congruence.
assert (hi' = hi) by congruence.
subst.
inversion H1. inversion H2. inversion H1'. inversion H2'.
assert (v2 = v1') by congruence.
subst. cbn. rewrite (Qeq_eqR _ _ chk2). rewrite (Qeq_eqR _ _ chk1).
exists v1'. repeat split; auto.
+ apply andb_prop in chk. destruct chk as [chk chk0].
apply (IHl _ chk0); tauto.
checkPre P q = true ->
eval_smt_logic E q ->
eval_precond E P.
Proof.
intros Heq Hq.
apply smt_to_pre_correct.
now apply (SMTLogic_eqb_sound _ _ _ Heq).
Qed.
*)
Lemma precond_bound_correct E P preQ bound :
eval_precond E P ->
......@@ -638,6 +546,7 @@ Proof.
eapply checkPre_pre_smt; eauto.
Qed.
(* unsat queries of appropriate form yield bounds *)
Lemma RangeBound_low_sound E P preQ e r Gamma v :
eval_precond E P ->
checkPre P preQ = true ->
......@@ -650,7 +559,7 @@ Proof.
apply Rnot_lt_le. intros B.
apply H2. eapply precond_bound_correct; eauto.
split; cbn; auto.
do 2 eexists. repeat split; first [eassumption | constructor].
exists v, (Q2R r). repeat split; auto. constructor.
Qed.
Lemma RangeBound_high_sound E P preQ e r Gamma v :
......@@ -665,5 +574,5 @@ Proof.
apply Rnot_lt_le. intros B.
apply H2. eapply precond_bound_correct; eauto.
split; cbn; auto.
do 2 eexists. repeat split; first [eassumption | constructor].
exists (Q2R r), v. repeat split; auto. constructor.
Qed.
......@@ -17,6 +17,7 @@ From Flover
Require Export IntervalArithQ IntervalArith SMTArith ssaPrgs
RealRangeArith.
(* let_env is used to store the mapping [x |-> f] when encountering function (let x := f in g) *)
Definition let_env := nat -> option (expr Q).
Definition lets_sound L E Gamma :=
......@@ -40,9 +41,9 @@ Fixpoint inlineLets (L: let_env) (e: expr Q) :=
| Fma e1 e2 e3 => Fma (inlineLets L e1) (inlineLets L e2) (inlineLets L e3)
| Downcast m e' => Downcast m (inlineLets L e')
| Let m x e1 e2 => Let m x (inlineLets L e1) (inlineLets L e2)
(* | Cond e1 e2 e3 => Cond (inlineLets L e1) (inlineLets L e2) (inlineLets L e3) *)
end.
(* inlineLets preserves evaluation for reasonable let_env *)
Lemma inlineLets_sound L E Gamma inVars outVars e v :
lets_sound L E Gamma ->
(forall x e, L x = Some e -> NatSet.Subset (NatSet.add x (freeVars e)) inVars) ->
......@@ -112,19 +113,6 @@ Proof.
apply H4. eapply LfVars_valid; eauto.
set_tac. }
* now extended_ssa.
(*
- inversion H; subst.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
inversion ssa_e; subst.
subst.
assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. eapply Cond_then; eauto.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
inversion ssa_e; subst.
subst.
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. eapply Cond_else; eauto.
*)
Qed.
Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) P L :=
......@@ -141,6 +129,7 @@ Definition tightenUpperBound (e: expr Q) (hi: Q) (q: SMTLogic) P L :=
| _ => hi
end.
(* try to tighten the given interval using correct encoded queries *)
Definition tightenBounds (e: expr Q) (iv: intv) (qMap: usedQueries) P L :=
match FloverMap.find e qMap with
| None => iv
......@@ -204,6 +193,7 @@ Proof.
exact H.
Qed.
(* tightening using appropriate unsat queries is sound *)
Lemma tightenBounds_sound E Gamma e v iv qMap P L :
eval_precond E P ->
(forall ql qh, FloverMap.find e qMap = Some (ql, qh) ->
......@@ -220,6 +210,8 @@ Proof.
intros. edestruct unsatQ; eauto.
Qed.
(* the final validator is essentially the interval arithmetic validator,
except that in each step 'tightenBounds' is applied *)
Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
(Q: usedQueries) L (validVars: NatSet.t) : bool :=
match FloverMap.find e A with
......@@ -319,23 +311,11 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
| _, _, _ => false
end
else false
(* | Cond f1 f2 f3 => false *)
(*
if ((validSMTIntervalbounds f1 A P validVars) &&
(validSMTIntervalbounds f2 A P validVars) &&
(validSMTIntervalbounds f3 A P validVars))
then
match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with
| Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
let new_iv := (* TODO *) in
isSupersetIntv new_iv intv
| _, _, _ => false
end
else false
*)
end
end.
(* soundness proof is essentially the same as the one for interval arithmetic,
except in each step 'tightenBounds_sound' is applied *)
Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: precond)
(Q: usedQueries) L fVars dVars outVars (E: env) Gamma :
unsat_queries Q ->
......
......@@ -6,6 +6,7 @@ From Flover
Require Import List FunInd Sorting.Permutation Sorting.Mergesort Orders.
(* define relation on the analysis results, such that validity carries over *)
Fixpoint resultLeq e (A1 A2: analysisResult) :=
match e with
| Unop _ e1 | Downcast _ e1 => resultLeq e1 A1 A2
......@@ -56,6 +57,7 @@ Proof.
- apply (reflect_iff _ _ (Z.leb_spec0 _ _)). auto.
Qed.
(* validRanges carries over *)
Lemma resultLeq_range_sound e A1 A2 E Gamma :
resultLeq e A1 A2 = true ->
validRanges e A1 E Gamma ->
......@@ -145,6 +147,7 @@ Proof.
repeat split; auto; lra.
Qed.
(* validErrorBounds carries over *)
Lemma resultLeq_error_sound e A1 A2 E1 E2 Gamma :
resultLeq e A1 A2 = true ->
validErrorBounds e E1 E2 A1 Gamma ->
......@@ -268,7 +271,6 @@ Proof.
lra.
Qed.
(* TODO: maybe put this somewhere else *)
Lemma approxEnv_empty_dVars A1 A2 Gamma fVars dVars E1 E2 :
NatSet.Empty dVars ->
approxEnv E1 Gamma A1 fVars dVars E2 ->
......@@ -281,6 +283,7 @@ Proof.
- exfalso. eapply He. set_tac.
Qed.
(* run checker on subdomain and check the above relation *)
Definition checkSubdivsStep e absenv defVars Gamma (PAQ: precond * analysisResult * usedQueries) :=
match PAQ with
| (P, A, Q) =>
......@@ -318,38 +321,15 @@ Proof.
now apply andb_true_iff in H as [H1 H2].
Qed.
Fixpoint coverIntv iv intvs :=
match intvs with
| nil => false
| intv :: nil => isSupersetIntv iv intv
| intv :: intvs =>
Qleb (ivlo intv) (ivlo iv) && coverIntv (ivhi intv, ivhi iv) intvs
end.
Lemma coverIntv_sound iv intvs v :
coverIntv iv intvs = true ->
(Q2R (ivlo iv) <= v <= Q2R (ivhi iv))%R ->
exists intv, In intv intvs /\ (Q2R (ivlo intv) <= v <= Q2R (ivhi intv))%R.
Proof.
induction intvs as [|intv0 intvs] in iv |- *; [intros H; discriminate H|].
destruct intvs as [|intv1 intvs]; cbn; intros H Hin.
- exists intv0. split; auto. andb_to_prop H. canonize_hyps. cbn in *. lra.
- destruct (Rle_or_lt v (Q2R (ivhi intv0))) as [Hle|Hlt].
+ andb_to_prop H.
canonize_hyps.
exists intv0. split; cbn; auto.
cbn in *. lra.
+ andb_to_prop H.
destruct (IHintvs (ivhi intv0, ivhi iv)) as [intv [inl Hin1]]; eauto.
cbn in *. lra.
Qed.
(* remove the preconds 'P' from 'Ps' that have contraint 'iv' for input 'x';
from those 'P' remove this constraint and collect them in 'sl';
other 'P' are collected in 'rest' *)
Fixpoint getSlice x iv Ps :=
match Ps with
| nil => (nil, nil)
| P :: Ps' =>
match P with
| nil => (nil, Ps) (* fail *)
| nil => (nil, Ps)
| (e, ivE) :: P' =>
if FloverMapFacts.P.F.eqb (Var Q x) e && isSupersetIntv iv ivE then
let (sl, rest) := getSlice x iv Ps' in (P' :: sl, rest)
......@@ -370,6 +350,7 @@ Proof with try now injection 1; intros; subst.
cbn. now rewrite <- IHPs.
Qed.
(* from precond 'P' in slice 'sl', we can construct precond in Ps *)
Lemma getSlice_sound x iv Ps sl rest :
getSlice x iv Ps = (sl, rest) ->
forall P, In P sl ->
......@@ -388,6 +369,7 @@ Proof with try now injection 1; intros; subst.
- edestruct IHPs as [ivx [inPs sub]]; eauto.
Qed.
(* 'rest' is subset 'Ps' *)
Lemma getSlice_rest_sound x iv Ps sl rest :
getSlice x iv Ps = (sl, rest) ->
forall P, In P rest -> In P Ps.
......@@ -401,6 +383,7 @@ Proof with try now injection 1; intros; subst.
right. eapply IHPs; eauto.
Qed.
(* for 'P' in 'Ps', there are only the two cases above *)
Lemma getSlice_complete x iv Ps sl rest :
getSlice x iv Ps = (sl, rest) ->
forall P, In P Ps ->
......@@ -421,42 +404,7 @@ Proof with try now injection 1; intros; subst; auto.
right. exists P1, ivx. split; auto. now constructor 2.
Qed.
(*
Function checkDim cov x iv Ps {measure length Ps} :=
match Ps with
| nil => false
| P :: _ =>
match FloverMap.find (Var Q x) P with
| Some ivx =>
let (b, rest) := getSlice_aux x ivx Ps in
let covb := cov b in
covb && match rest with
| nil => isSupersetIntv iv ivx
| _ => checkDim cov x (snd ivx, snd iv) rest
end
| None => false
end
end.
intros cov x iv Ps P Ps' HPs ivx Hfind b rest P' rest' Hrest.
rewrite <- Hrest.
rewrite <- HPs at 2.
cbn.
unfold addToSlice.
rewrite Hfind.
unfold isSupersetIntv, Qleb, Qle_bool.
rewrite !Z.leb_refl.
rewrite <- HPs.
cbn.
destruct (getSlice_aux x ivx Ps') eqn:Heq.
apply getSlice_aux_sound in Heq.
clear Hrest rest'.
injection 1; intros; subst.
cbn.
rewrite Heq, app_length.
apply le_lt_n_Sm, le_plus_r.
Defined.
*)
(* checks all slices of variable 'x' with function 'cov' *)
Function checkDim cov x iv Ps {measure length Ps} :=
match Ps with
| nil => false
......@@ -488,6 +436,7 @@ rewrite app_length.
apply le_lt_n_Sm, le_plus_r.
Defined.
(* check the slices of var 'x' recursively *)
Fixpoint covers (P: list (expr Q * intv)) Ps :=
match P with
| nil => match Ps with nil::nil => true | _ => false end
......@@ -496,6 +445,7 @@ Fixpoint covers (P: list (expr Q * intv)) Ps :=
| _ :: P => false
end.
(* a input has to be in one subdomain if subdomains cover global domain *)
Lemma covers_sound P Ps E :
covers P Ps = true ->
eval_preIntv E P ->
......@@ -578,6 +528,8 @@ Proof.
eapply IHP; eauto.
Qed.
(* order the subdomains lexicographically, such that the above algorithm
works as intended *)
Module PrecondOrder <: TotalLeBool.
Definition t := list (expr Q * intv).
......@@ -610,11 +562,10 @@ Definition checkPreconds (subdivs: list precond) (P: precond) :=
let Piv := FloverMap.elements (fst P) in
let Ps := map (fun P => FloverMap.elements (fst P)) subdivs in
let S_qs := map snd subdivs in
(* Check that join of the preconditions for the subdivisions
covers the global precondition *)
(* check that subdomains cover global domain *)
covers Piv (sort Ps) &&
(* Check that additional constraints encoded by Daisy agree
for each subdivision *)
(* check that additional constraints for the subdomain agree
with the one for the global domain *)
forallbTailrec (fun q => SMTLogic_eqb q (snd P)) S_qs.
Lemma checkPreconds_sound (subdivs: list precond) E P :
......@@ -654,18 +605,41 @@ Proof.
apply in_map_iff; eauto.
Qed.
(** Interval subdivisions checking function **)
(* check for emptiness as witnessed by a suitable query *)
Definition isNonEmptySubdiv e (S: precond * analysisResult * usedQueries) :=
match S with
| (P, A, Q) => match FloverMap.find e Q with
| Some (q, _) => negb (checkPre P q)
| None => true
end
end.
Lemma isNonEmptySubdiv_sound E e P A Q :
eval_precond E P ->
unsat_queries Q ->
isNonEmptySubdiv e (P, A, Q) = true.
Proof.
intros HP HQ. cbn.
destruct (FloverMap.find e Q) as [[q1 q2] |] eqn: Hfind; auto.
destruct (checkPre P q1) eqn: H; auto.
exfalso. destruct (HQ E e q1 q2) as [HnP _]; auto.
apply HnP.
eapply checkPre_pre_smt; eauto.
Qed.
(** interval subdivision checker function **)
Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
(P: precond) subdivs (defVars: FloverMap.t mType) Gamma :=
validSSA e (preVars P) &&
checkPreconds (map (fun S => match S with (P, _, _) => P end) subdivs) P &&
checkSubdivs e absenv subdivs defVars Gamma.
(* check results only for non-empty domains *)
checkSubdivs e absenv (filter (isNonEmptySubdiv e) subdivs) defVars Gamma.
Definition queriesInSubdivs (subdivs: list (precond * analysisResult * usedQueries)) :=
map (fun S => match S with (_, _, Q) => Q end) subdivs.
(**
Soundness proof for the interval subdivs checker.
soundness proof for the interval subdivision checker
**)
Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P subdivs defVars Gamma:
forall (E1 E2: env) DeltaMap,
......@@ -680,17 +654,6 @@ Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P subdivs de
validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\
validErrorBounds e E1 E2 absenv Gamma /\
validFPRanges e E2 Gamma DeltaMap.
(*
exists Gamma,
approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
exists iv err vR vF m,
FloverMap.find e absenv = Some (iv, err) /\
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) vR REAL /\
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m /\
(forall vF m,
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
*)
Proof.
intros * deltas_matched approxEnv P_valid unsat_qs valid_typeMap chk.
apply andb_prop in chk as [chk valid_subdivs].
......@@ -700,7 +663,11 @@ Proof.
{ eapply validSSA_eq_set; eauto. eapply checkPreconds_preVars; eauto. }
apply in_map_iff in in_subdivs as [[[P2 A] Qmap] [Heq in_subdivs]].
cbn in Heq; subst.
pose proof (checkSubdivs_sound e _ _ _ _ _ _ _ valid_subdivs in_subdivs) as [range_err_check A_leq].
assert (In (P1, A, Qmap) (filter (isNonEmptySubdiv e) subdivs)) as in_nonempty_subdivs.
{ apply filter_In. split; auto.
eapply isNonEmptySubdiv_sound; eauto.
apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
pose proof (checkSubdivs_sound e _ _ _ _ _ _ _ valid_subdivs in_nonempty_subdivs) as [range_err_check A_leq].
assert (ResultChecker e A P1 Qmap defVars Gamma = true) as res_check
by (unfold ResultChecker; now rewrite valid_ssa', range_err_check).