Commit 103c2686 authored by Heiko Becker's avatar Heiko Becker

Fix flaw in evaluation semantics, that would allow perturbed evaluations to ignore the precondition

parent fe76e068
......@@ -171,6 +171,7 @@ Proof.
rewrite Rabs_mult.
eapply Rle_trans;[ | apply error_valid].
apply Rmult_le_compat;try (apply Rabs_pos);[ | apply H2].
rewrite (delta_0_deterministic (cenv v) delta) in *; auto.
pose proof (Rle_trans (Q2R plo) (Q2R ivlo) (cenv v) plo_le_ivlo H1).
pose proof (Rle_trans (cenv v) (Q2R ivhi) (Q2R phi) H4 ivhi_le_phi).
pose proof (RmaxAbs (Q2R plo) (cenv v) (Q2R phi) H5 H6).
......
......@@ -119,7 +119,7 @@ Inductive eval_exp (eps:R) (E:env) (P:precond) : (exp R) -> R -> Prop :=
Var_load x: eval_exp eps E P (Var R x) (E x)
| Param_acc x delta:
((Rabs delta) <= eps)%R ->
((Q2R (fst (P x))) <= E x <= (Q2R (snd (P x))))%R ->
((Q2R (fst (P x))) <= perturb (E x) delta <= (Q2R (snd (P x))))%R ->
eval_exp eps E P (Param R x) (perturb (E x) delta)
| Const_dist n delta:
Rle (Rabs delta) eps ->
......
......@@ -174,6 +174,7 @@ Proof.
unfold Qleb in abslo_le_ivlo, ivhi_le_abshi.
apply Qle_bool_iff in abslo_le_ivlo; apply Qle_bool_iff in ivhi_le_abshi.
apply Qle_Rle in abslo_le_ivlo; apply Qle_Rle in ivhi_le_abshi.
rewrite delta_0_deterministic in *; auto.
split; lra.
- intros vR valid_bounds eval_f.
unfold validIntervalbounds in valid_bounds.
......
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