Skip to content

GitLab

Commit 412e1f64 authored by Nikita Zyuzin's avatar Nikita Zyuzin
Browse files

Merge branch 'master' of https://gitlab.mpi-sws.org/AVA/FloVer into errors_affine

parents e3568321 55c016cd
Hide whitespace changes
Inline Side-by-side
coq/ErrorAnalysis.v
View file @ 412e1f64
......@@ -44,11 +44,16 @@ Qed.
Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
match c with
| Let m x e k => validErrorBounds e E1 E2 A Gamma DeltaMap /\
(forall v__R v__FP,
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m ->
validErrorBoundsCmd k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap)
| Let m x e k =>
validErrorBounds e E1 E2 A Gamma DeltaMap /\
(exists iv_e err_e iv_x err_x,
FloverMap.find e A = Some (iv_e, err_e) /\
FloverMap.find (Var Q x) A = Some (iv_x, err_x) /\
Qeq_bool err_e err_x = true) /\
(forall v__R v__FP,
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m ->
validErrorBoundsCmd k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap)
| Ret e => validErrorBounds e E1 E2 A Gamma DeltaMap
end /\
forall v__R (iv: intv) (err: error),
......
coq/ErrorValidation.v
View file @ 412e1f64
......@@ -2070,7 +2070,7 @@ Proof.
eapply IHe1'; eauto.
- specialize typing_ok as (? & ?).
intuition.
- set_tac. split; set_tac.
- set_tac. split; set_tac.
- cbn in *; Flover_compute; try congruence; type_conv; subst;
destruct b; Flover_compute; try congruence.
- cbn in valid_intv.
......@@ -2082,7 +2082,7 @@ Proof.
eapply IHe2'; eauto.
- specialize typing_ok as (? & ?).
intuition.
- set_tac. split; set_tac.
- set_tac. split; set_tac.
- cbn in *; Flover_compute; try congruence; type_conv; subst;
destruct b; Flover_compute; try congruence.
- cbn in valid_intv.
......@@ -2175,7 +2175,7 @@ Proof.
eapply IHe1'; eauto.
- specialize typing_ok as (? & ?).
intuition.
- set_tac. split; set_tac.
- set_tac. split; set_tac.
- cbn in *; Flover_compute; try congruence; type_conv; subst;
destruct b; Flover_compute; try congruence.
- cbn in valid_intv.
......@@ -2186,7 +2186,7 @@ Proof.
eapply IHe2'; eauto.
- specialize typing_ok as (? & ?).
intuition.
- set_tac. split; set_tac.
- set_tac. split; set_tac.
- cbn in *; Flover_compute; try congruence; type_conv; subst;
destruct b; Flover_compute; try congruence.
- cbn in valid_intv.
......@@ -2197,7 +2197,7 @@ Proof.
eapply IHe3'; eauto.
- specialize typing_ok as (? & ?).
intuition.
- set_tac. split; set_tac.
- set_tac. split; set_tac.
- cbn in *; Flover_compute; try congruence; type_conv; subst;
destruct b; Flover_compute; try congruence.
- cbn in valid_intv.
......@@ -2445,8 +2445,9 @@ Proof.
by (eapply validErrorbound_sound; eauto).
split.
{
split.
repeat split.
- eapply validErrorbound_sound; eauto.
- repeat eexists. eauto.
- intros vR vF eval_real eval_float.
eapply validErrorBounds_single in Hsound; eauto.
destruct Hsound as [[vFe [mFe eval_float_e]] bounded_e].
......
coq/ErrorValidationAA.v
View file @ 412e1f64
......@@ -173,7 +173,7 @@ Fixpoint validErrorboundAA (e:expr Q) (* analyzed expression *)
let aaRangee2 := fromIntv ive2 maxNoise3 in
let aaRangee3 := fromIntv ive3 (maxNoise3 + 1) in
let propError := AffineArithQ.plus_aff
afPolye1
afPolye1
(AffineArithQ.subtract_aff
(AffineArithQ.plus_aff
(AffineArithQ.mult_aff aaRangee2 afPolye3 (maxNoise3 + 2))
......@@ -482,7 +482,7 @@ Proof.
destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
destruct p.
destruct (negb (Qleb 0 e0)) eqn: H0err; [congruence|].
destruct (negb (Qleb 0 e0)) eqn: H0err; [congruence|].
destruct u; [|congruence].
destruct (validErrorboundAA e Gamma A dVars noise1 expr_map1)
as [(subexpr_map, subnoise)|] eqn: Hvalidsubexpr;
......@@ -520,7 +520,7 @@ Proof.
destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
destruct p as (? & err__A).
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (validErrorboundAA e1 Gamma A dVars noise1 expr_map1)
as [(subexpr_map1, subnoise1)|] eqn: Hvalidsubexpr1;
cbn in Hvalidbounds; try congruence.
......@@ -652,7 +652,7 @@ Proof.
destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
destruct p as (? & err__A).
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (validErrorboundAA e1 Gamma A dVars noise1 expr_map1)
as [(subexpr_map1, subnoise1)|] eqn: Hvalidsubexpr1;
cbn in Hvalidbounds; try congruence.
......@@ -746,7 +746,7 @@ Proof.
destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
destruct p.
destruct (negb (Qleb 0 e0)) eqn: H0err; [congruence|].
destruct (negb (Qleb 0 e0)) eqn: H0err; [congruence|].
destruct (validErrorboundAA e Gamma A dVars noise1 expr_map1)
as [(subexpr_map, subnoise)|] eqn: Hvalidsubexpr;
cbn in Hvalidbounds; try congruence.
......@@ -779,7 +779,7 @@ Qed.
Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVars :=
forall (expr_map1 expr_map2 : FloverMap.t (affine_form Q))
(noise_map1 : nat -> option noise_type) (noise1 noise2 : nat) (v__R : R)
(noise_map1 : nat -> option noise_type) (noise1 noise2 : nat) (v__R : R)
(iv__A : intv) (err__A : error),
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
......@@ -861,7 +861,7 @@ Proof.
replace tmperr with err__A in * by congruence; clear Hres__A' tmperr tmpiv.
eapply meps_0_deterministic in Heval1'; try exact Heval__R.
replace tmpvR with v__R in * by congruence; clear Heval1' tmpvR.
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
cbn in Htypecheck.
destruct (NatSet.mem n dVars) eqn: Hmem__n; cbn in Hvalidbounds.
- inversion Hvalidbounds; subst; clear Hvalidbounds.
......@@ -871,7 +871,7 @@ Proof.
congruence.
- destruct (Qleb (computeErrorQ (maxAbs iv__A) m) err__A) eqn: Herrle; cbn in Hvalidbounds; [|congruence].
inversion Hvalidbounds; subst; clear Hvalidbounds.
rewrite mem_false_find_none in Hmem.
rewrite mem_false_find_none in Hmem.
apply not_in_not_mem in Hmem__n.
assert (n ∈ fVars) as Hmem__n' by (set_tac; set_tac).
assert (exists v, E2 n = Some v) as [v__fp Hv__fp]
......@@ -917,7 +917,7 @@ Proof.
exists (mkErrorPolyQ (computeErrorQ (maxAbs iv__A) m__FP) noise1),
(Q2R (computeErrorQ (maxAbs iv__A) m__FP)), (updMap noise_map1 noise1 q).
rewrite computeErrorQ_computeErrorR in Herrle |-*.
{
{
repeat split; try auto.
- now apply contained_flover_map_extension.
- lia.
......@@ -945,7 +945,7 @@ Proof.
exists (mkErrorPolyQ (computeErrorQ (maxAbs iv__A) m__FP) noise1),
(Q2R (computeErrorQ (maxAbs iv__A) m__FP)).
rewrite computeErrorQ_computeErrorR.
{
{
repeat split; try auto.
- rewrite afQ2R_mkErrorPolyQ.
apply mkErrorPolyR_fresh_compat; lia.
......@@ -970,7 +970,7 @@ Proof.
erewrite eval_expr_functional with (v1 := v__FP0) (v2 := v__FP); eauto.
erewrite Gamma_det; eauto.
}
}
}
Qed.
Lemma validErrorboundAA_sound_const v m E1 E2 A Gamma DeltaMap fVars dVars:
......@@ -999,7 +999,7 @@ Proof.
destruct (Htypecheck) as (m__e & Hetype & _ & Hvalidexec).
rewrite Hetype in Hvalidbounds; simpl in Hvalidbounds.
rewrite Hcert in Hvalidbounds; cbn in Hvalidbounds.
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (Qleb (computeErrorQ (maxAbs iv__A) m) err__A) eqn: Herrle; cbn in Hvalidbounds; [|congruence].
inversion Hvalidbounds; subst; clear Hvalidbounds.
rewrite mem_false_find_none in Hmem.
......@@ -1073,7 +1073,7 @@ Proof.
+ apply contained_map_extension; auto.
+ rewrite FloverMapFacts.P.F.add_eq_o; try auto.
apply Q_orderedExps.exprCompare_refl.
+ apply computeErrorR_pos.
+ apply computeErrorR_pos.
+ rewrite afQ2R_mkErrorPolyQ.
rewrite computeErrorQ_computeErrorR.
rewrite toInterval_mkErrorPolyR; auto using computeErrorR_pos.
......@@ -1134,7 +1134,7 @@ Proof.
destruct Htypecheck as (m__e & Hetype & (Htypecheck__e & ?) & Hvalidexec).
rewrite Hetype in Hvalidbounds; simpl in Hvalidbounds.
rewrite Hcert in Hvalidbounds; simpl in Hvalidbounds.
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct u; [|congruence].
destruct (validErrorboundAA e Gamma A dVars noise1 expr_map1)
as [(subexpr_map, subnoise)|] eqn: Hvalidsubexpr;
......@@ -1149,7 +1149,7 @@ Proof.
unfold isCompat in H2.
destruct m; cbn in H2; try congruence; clear H2.
pose proof H3 as H3det.
specialize (IHe expr_map1 subexpr_map noise_map1 noise1 noise2 v1 subiv suberr).
specialize (IHe expr_map1 subexpr_map noise_map1 noise1 noise2 v1 subiv suberr).
specialize IHe as (IHevex & IHevall); eauto;
[destruct Hrange; auto|].
split.
......@@ -1279,7 +1279,7 @@ Proof.
destruct (Htypecheck) as (m__e & find_t & (Htypecheck1 & Htypecheck2 & Hjoin) & valid_exec).
rewrite find_t in Hvalidbounds.
rewrite Hcert in Hvalidbounds; cbn in Hvalidbounds.
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (validErrorboundAA e1 Gamma A dVars noise1 expr_map1)
as [(subexpr_map1, subnoise1)|] eqn: Hvalidsubexpr1;
cbn in Hvalidbounds; try congruence.
......@@ -1545,7 +1545,7 @@ Proof.
destruct (Htypecheck) as (m__e & find_t & (Htypecheck1 & Htypecheck2 & Hjoin) & valid_exec).
rewrite find_t in Hvalidbounds.
rewrite Hcert in Hvalidbounds; cbn in Hvalidbounds.
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (validErrorboundAA e1 Gamma A dVars noise1 expr_map1)
as [(subexpr_map1, subnoise1)|] eqn: Hvalidsubexpr1;
cbn in Hvalidbounds; try congruence.
......@@ -1789,7 +1789,7 @@ Proof.
destruct (Htypecheck) as (m__e & find_t & (Htypecheck1 & Htypecheck2 & Hjoin) & valid_exec).
rewrite find_t in Hvalidbounds.
rewrite Hcert in Hvalidbounds; cbn in Hvalidbounds.
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (validErrorboundAA e1 Gamma A dVars noise1 expr_map1)
as [(subexpr_map1, subnoise1)|] eqn: Hvalidsubexpr1;
cbn in Hvalidbounds; try congruence.
......@@ -2083,7 +2083,7 @@ Proof.
destruct (Htypecheck) as (m__e & find_t & (Htypecheck1 & Htypecheck2 & Hjoin) & valid_exec).
rewrite find_t in Hvalidbounds.
rewrite Hcert in Hvalidbounds; cbn in Hvalidbounds.
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (validErrorboundAA e1 Gamma A dVars noise1 expr_map1)
as [(subexpr_map1, subnoise1)|] eqn: Hvalidsubexpr1;
cbn in Hvalidbounds; try congruence.
......@@ -2128,17 +2128,17 @@ Proof.
(AffineArithQ.plus_aff
(AffineArithQ.subtract_aff
(AffineArithQ.mult_aff subaf1
(fromIntv (invertIntv iv2) (subnoise2 + 1))
(fromIntv (invertIntv iv2) (subnoise2 + 1))
(subnoise2 + 4))
(AffineArithQ.mult_aff (fromIntv iv1 subnoise2)
(AffineArithQ.mult_aff subaf2
(fromIntv (invertIntv (multIntv iv2 (widenIntv iv2 err2)))
(subnoise2 + 2)) (subnoise2 + 3))
(subnoise2 + 2)) (subnoise2 + 3))
(subnoise2 + 5)))
(AffineArithQ.mult_aff subaf1
(AffineArithQ.mult_aff subaf2
(fromIntv (invertIntv (multIntv iv2 (widenIntv iv2 err2)))
(subnoise2 + 2)) (subnoise2 + 3))
(subnoise2 + 2)) (subnoise2 + 3))
(subnoise2 + 6)))
(mkErrorPolyQ
(computeErrorQ
......@@ -2461,7 +2461,7 @@ Proof.
& valid_exec).
rewrite find_t in Hvalidbounds.
rewrite Hcert in Hvalidbounds; cbn in Hvalidbounds.
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (validErrorboundAA e1 Gamma A dVars noise1 expr_map1)
as [(subexpr_map1, subnoise1)|] eqn: Hvalidsubexpr1;
cbn in Hvalidbounds; try congruence.
......@@ -2847,7 +2847,7 @@ Proof.
subst.
rewrite Hetype in Hvalidbounds; cbn in Hvalidbounds.
rewrite Hcert in Hvalidbounds; cbn in Hvalidbounds.
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
destruct (validErrorboundAA e Gamma A dVars noise1 expr_map1)
as [(subexpr_map, subnoise)|] eqn: Hvalidsubexpr;
cbn in Hvalidbounds; try congruence.
......@@ -2953,7 +2953,7 @@ Proof.
apply Rmax_case; apply Rabs_pos.
* symmetry; erewrite RmaxAbsFun_iv; auto; try apply radius_nonneg.
eauto 9
using plus_aff_to_interval_sym_compat,
using plus_aff_to_interval_sym_compat,
toInterval_mkErrorPolyR, computeErrorR_pos, RmaxAbsFun_iv, radius_nonneg.
* intros e' Hnin Hin.
{
......@@ -2980,7 +2980,7 @@ Proof.
apply Rmax_case; apply Rabs_pos.
+ symmetry; erewrite RmaxAbsFun_iv; auto; try apply radius_nonneg.
eauto 3
using plus_aff_to_interval_sym_compat,
using plus_aff_to_interval_sym_compat,
toInterval_mkErrorPolyR, computeErrorR_pos, RmaxAbsFun_iv, radius_nonneg.
+ erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
now match goal with
......@@ -3005,7 +3005,7 @@ Theorem validErrorboundAA_sound (e: expr Q) E1 E2 A Gamma DeltaMap fVars dVars:
validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVars.
Proof.
induction e.
- apply validErrorboundAA_sound_var; auto.
- apply validErrorboundAA_sound_var; auto.
- apply validErrorboundAA_sound_const; auto.
- apply validErrorboundAA_sound_unop; auto.
- apply validErrorboundAA_sound_binop; auto.
......@@ -3401,6 +3401,7 @@ Proof.
}
specialize (Hvalidall__e v__FP m__FP Heval__e) as (af__e & err__e & noise_map2 & ? & ? & ? & ? & ? & ? &
? & Hiv & ? & Hevals & Hcheckedall__e).
pose proof Heqerr as Heqerr_bool.
rewrite Qeq_bool_iff in Heqerr.
apply Qeq_eqR in Heqerr.
assert (approxEnv (updEnv n v E1) (toRExpMap Gamma) A fVars
......@@ -3633,6 +3634,8 @@ Proof.
}
edestruct validErrorboundAA_contained_subexpr as (? & ? & ?);
try exact Hvalidbounds'; eauto.
* exists subiv, suberr, variv, varerr.
repeat split; auto.
* intros v__R0 v__FP0 Heval__R0 Heval__FP0.
apply eval_expr_functional with (v1 := v) in Heval__R0; eauto.
apply eval_expr_functional with (v1 := v__FP) in Heval__FP0; eauto.
......
coq/FPRangeValidator.v
View file @ 412e1f64
......@@ -166,10 +166,7 @@ Proof.
induction f; intros;
simpl in *;
(match_pat (bstep _ _ (toRTMap _) _ _ _) (fun H => inversion H; subst; simpl in * ));
(match_pat (bstep _ _ (toRExpMap Gamma) _ _ _) (fun H => inversion H; subst; simpl in * ));
repeat match goal with
| H : _ = true |- _ => andb_to_prop H
end.
(match_pat (bstep _ _ (toRExpMap Gamma) _ _ _) (fun H => inversion H; subst; simpl in * )).
- destruct H4
as [[me [find_me [find_var [? [validt_e validt_f]]]]] valid_exec].
assert (m = me) by (eapply validTypes_exec in find_me; eauto); subst.
......@@ -198,9 +195,11 @@ Proof.
apply (IHf (updEnv n vR_e E1) (updEnv n v1 E2)
Gamma DeltaMap v vR m0 A fVars
(NatSet.add n dVars) (outVars)); eauto.
* eapply approxUpdBound; eauto; simpl in *.
* destruct validerr_rec as [[iv_e2 [err_e2 [iv_x [err_x [find_e [find_x eqfind]]]]]] validerr_rec].
rewrite find_e in *; canonize_hyps. inversion map_e; subst.
eapply approxUpdBound; eauto; simpl in *.
{ eapply toRExpMap_some; eauto. simpl; auto. }
{ admit. }
{ rewrite <- eqfind. eapply err_bounded_e. eauto. }
* eapply ssa_equal_set; eauto.
hnf. intros a; split; intros in_set.
{ rewrite NatSet.add_spec, NatSet.union_spec;
......@@ -216,6 +215,7 @@ Proof.
{ intros x; unfold toRMap, updDefVars.
destruct (x =? n) eqn:?; auto. }
{ eapply valid_rec. auto. } *)
* destruct validerr_rec; auto.
* set_tac; split.
{ split; try auto.
hnf; intros; subst.
......@@ -244,4 +244,4 @@ Proof.
rewrite NatSet.add_spec in H5; destruct H5;
auto; subst; congruence. }
- destruct H5. destruct H4. destruct H6. eapply FPRangeValidator_sound; eauto.
Admitted.
Qed.
coq/IEEE_connection.v
View file @ 412e1f64
......@@ -885,8 +885,8 @@ Proof.
assert (exists iv err, FloverMap.find (B2Qexpr e) A = Some (iv, err)) as Hcert.
{
intuition.
eapply validRanges_single in H10.
destruct H10 as (? & ? & ? & ? & ?); eauto.
eapply validRanges_single in H12.
destruct H12 as (? & ? & ? & ? & ?); eauto.
}
specialize Hcert as (? & ? & Hcert).
pose proof valid_error as valid_error'.
......@@ -913,9 +913,11 @@ Proof.
vR vF_new A fVars (NatSet.add n dVars) outVars); try eauto.
+ intros. unfold toREnv, updFlEnv, updEnv.
destruct (x1 =? n); auto. rewrite <- envs_eq. unfold toREnv; auto.
+ eapply approxUpdBound; eauto.
+ destruct valid_error_cmd as [[? [? [? [? [? [? ?]]]]]] ?].
eapply approxUpdBound; eauto.
* eapply toRExpMap_some with (e:=Var Q n); eauto.
* admit.
* canonize_hyps. rewrite Hcert in *. inversion H1; subst.
lra.
+ eapply ssa_equal_set; eauto.
hnf; split; intros.
* rewrite NatSet.add_spec, NatSet.union_spec in *.
......
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