Commit dfa6afde authored by Heiko Becker's avatar Heiko Becker

WIP FPRangeValidator soundness in Coq

parent c7165590
(* TODO: Flocq ops open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory *)
Require Import Coq.QArith.QArith.
Require Import Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.MachineType Daisy.Typing Daisy.Infra.RealSimps Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Commands Daisy.Environments Daisy.ssaPrgs.
......@@ -49,4 +49,69 @@ Fixpoint FPRangeValidatorCmd (f:cmd Q) (A:analysisResult) typeMap dVars :=
then FPRangeValidatorCmd g A typeMap (NatSet.add n dVars)
else false
| Ret e => FPRangeValidator e A typeMap dVars
end.
\ No newline at end of file
end.
Theorem FpRangeValidator_sound:
forall (e:exp Q) E1 E2 Gamma v m A tMap P fVars dVars,
approxEnv E1 Gamma A fVars dVars E2 ->
eval_exp E2 Gamma (toRExp e) v m ->
typeCheck e Gamma tMap = true ->
validIntervalbounds e A P dVars = true ->
validErrorbound e tMap A dVars = true ->
FPRangeValidator e A tMap dVars = true ->
NatSet.Subset (NatSet.diff (usedVars e) dVars) fVars ->
(forall v, NatSet.In v fVars ->
exists vR, E1 v = Some vR /\ Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R ->
(forall v, NatSet.In v fVars \/ NatSet.In v dVars ->
exists m, Gamma v = Some m) ->
(forall v, NatSet.In v dVars ->
exists vR, E1 v = Some vR /\
Q2R (fst (fst (A (Var Q v)))) <= vR <= Q2R (snd (fst (A (Var Q v)))))%R ->
(forall v, NatSet.In v dVars ->
exists vF m, E2 v = Some vF /\ tMap (Var Q v) = Some m /\ validFloatValue vF m) ->
validFloatValue v m.
Proof.
intros *.
unfold FPRangeValidator.
intros.
destruct (A e) as [iv_e err_e] eqn:?;
destruct iv_e as [e_lo e_hi] eqn:?; simpl in *.
assert (tMap e = Some m)
by (eapply typingSoundnessExp; eauto).
subst; simpl in *.
unfold validFloatValue.
assert (exists vR, eval_exp E1 (toRMap Gamma) (toREval (toRExp e)) vR M0 /\
Q2R (fst (fst (A e))) <= vR <= Q2R (snd (fst (A e))))%R.
{ eapply validIntervalbounds_sound; eauto.
- intros; apply H8.
rewrite <- NatSet.mem_spec; auto.
- intros. apply H6.
rewrite <- NatSet.mem_spec; auto.
- intros. apply H7.
set_tac.
rewrite <- NatSet.union_spec; auto. }
\\ `abs (vR - v) <= SND (A e)`
by (drule validErrorbound_sound
\\ rpt (disch_then drule)
\\ strip_tac
\\ qpat_x_assum `eval_exp E2 Gamma e nF _` kall_tac
\\ first_x_assum drule
\\ rw_asm_star `A e = _`)
\\ rw_asm_star `A e = _`
\\ qspecl_then [`vR`, `v`, `err_e`, `(e_lo,e_hi)`]
impl_subgoal_tac
(SIMP_RULE std_ss [contained_def, widenInterval_def] distance_gives_iv)
\\ fs[IVlo_def, IVhi_def]
\\ Cases_on `e`
>- (fs[]
>- (fs[validFloatValue_def]
\\ first_x_assum (qspecl_then [`n`] impl_subgoal_tac) \\ fs[domain_lookup]
\\ `tMap (Var n) = SOME m` by (drule typingSoundnessExp \\ rpt (disch_then drule)
\\ fs[])
\\ qpat_x_assum `tMap (Var n) = SOME _` (fn thm => fs[thm])
\\ inversion `eval_exp E2 _ _ _ _` eval_exp_cases
\\ qpat_x_assum `E2 n = SOME v` (fn thm => fs[thm])
\\ rveq \\ fs[])
\\ solve_tac)
\\ solve_tac);
......@@ -183,16 +183,24 @@ Definition minDenormalValue (m:mType) :=
Definition normal (v:Q) (m:mType) :=
Qle_bool (minValue m) (Qabs v) && Qle_bool (Qabs v) (maxValue m).
Definition denormal (v:Q) (m:mType) :=
Qle_bool (minValue m) (Qabs v) && Qle_bool (Qabs v) (maxValue m).
Definition Normal (v:R) (m:mType) :=
(Q2R (minValue m) <= (Rabs v) /\ (Rabs v) <= Q2R (maxValue m))%R.
Definition Denormal (v:R) (m:mType) :=
(Q2R (minValue m) <= (Rabs v) /\ (Rabs v) <= Q2R (maxValue m))%R.
(**
Predicate that is true if and only if the given value v is a valid
floating-point value according to the the type m.
Since we use the 1 + 𝝳 abstraction, the value must either be
in normal range or 0.
**)
Definition validFloatValue (v:Q) (m:mType) :=
Definition validFloatValue (v:R) (m:mType) :=
match m with
| M0 => true
| _ => normal v m || Qeq_bool v 0
| M0 => True
| _ => Normal v m \/ Denormal v m \/ v = 0%R
end.
Definition validValue (v:Q) (m:mType) :=
......
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