Commit b6ddcee8 authored by Joachim Bard's avatar Joachim Bard
Browse files

more comments

parent d4df3d07
......@@ -21,7 +21,8 @@ Inductive SMTArith :=
| TimesQ (e1 e2: SMTArith) : SMTArith
| DivQ (e1 e2: SMTArith) : SMTArith.
(* comparisons of restricted functions, as well as usual boolean connectives *)
(* 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
......@@ -45,7 +46,7 @@ Definition getBound q :=
| _ => None
end.
(* semantics for restricted functions *)
(* 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)
......@@ -261,7 +262,6 @@ Proof.
destruct m1; try discriminate.
now apply IHe'.
- cbn. congruence.
(* - cbn. congruence. *)
Qed.
Lemma eval_smt_expr E e v :
......@@ -369,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.
......@@ -450,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 :=
......@@ -544,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 ->
......
......@@ -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,7 +41,6 @@ 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 *)
......@@ -193,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) ->
......@@ -310,24 +311,10 @@ 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 essnetially the same as the one for interval arithmetic,
(* 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 :
......
......@@ -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,6 +605,7 @@ Proof.
apply in_map_iff; eauto.
Qed.
(* 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
......@@ -675,18 +627,19 @@ Proof.
eapply checkPre_pre_smt; eauto.
Qed.
(** Interval subdivisions checking function **)
(** 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 &&
(* 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,
......@@ -701,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].
......@@ -733,28 +675,3 @@ Proof.
{ apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
repeat split; eauto using resultLeq_range_sound, resultLeq_error_sound.
Qed.
(*
exists Gamma; intros approxE1E2.
assert (approxEnv E1 (toRExpMap Gamma) A (freeVars e) NatSet.empty E2) as approxE1E2'
by (eapply approxEnv_empty_dVars; eauto).
assert (validRanges e A E1 (toRTMap (toRExpMap Gamma))) as validRange.
{ edestruct result_checking_sound; eauto; [| intuition].
apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
assert (validErrorBounds e E1 E2 A Gamma) as Hsound.
{ edestruct result_checking_sound; eauto; [| intuition].
apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
eapply validRanges_single in validRange.
destruct validRange as [iv [err [vR [Hfind [eval_real validRange]]]]].
eapply validErrorBoundsRec_single in Hsound; eauto.
destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto.
destruct (resultLeq_sound _ _ _ A_leq) as [iv1 [err1 [iv2 [err2 H]]]].
destruct H as [F1 [F2 [sub err_leq]]].
exists iv2, err2, vR, vF, mF; repeat split; auto.
assert (err = err1) by congruence; subst.
apply Qle_Rle in err_leq.
intros vF0 m Heval.
specialize (err_bounded vF0 m Heval).
lra.
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