Commit 55c0ef90 authored by Nikita Zyuzin's avatar Nikita Zyuzin

[WIP] Change FloVer to use only deterministic semantics

parent 4614ca0c
This diff is collapsed.
......@@ -77,11 +77,17 @@ Proof.
destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
destruct iv_e as [elo ehi].
exists Gamma; intros approxE1E2.
edestruct (RoundoffErrorValidator_sound e H approxE1E2 H1 eval_real R
valid_e map_e)
as [[vF [mF eval_float]] err_bounded]; auto.
exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto.
Qed.
rewrite <- eval_expr_REAL_det_nondet in eval_real.
assert (forall (e' : expr Rdefinitions.R) (m' : mType),
exists d, (fun e m => Some 0%R) e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) as Htmp by admit.
assert (dVars_contained NatSet.empty (FloverMap.empty (affine_form Q))) as Hdvars
by (unfold dVars_contained; intros * Hset; clear - Hset; set_tac).
pose proof (RoundoffErrorValidator_sound e _ Htmp H approxE1E2 H1 eval_real R
valid_e map_e Hdvars) as Hsound.
unfold validErrorBounds in Hsound.
(* destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto. *)
(* exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto. *)
Admitted.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond)
defVars :=
......
......@@ -48,14 +48,15 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
Define big step semantics for the Flover language, terminating on a "returned"
result value
**)
Inductive bstep : cmd R -> env -> (expr R -> option mType) -> R -> mType -> Prop :=
let_b m m' x e s E v res defVars:
eval_expr E defVars e v m ->
bstep s (updEnv x v E) defVars res m' -> (* (updDefVars (Var R x) m defVars) res m' -> *)
bstep (Let m x e s) E defVars res m'
|ret_b m e E v defVars:
eval_expr E defVars e v m ->
bstep (Ret e) E defVars v m.
Inductive bstep : cmd R -> env -> (expr R -> option mType) -> (expr R -> mType -> option R) ->
R -> mType -> Prop :=
let_b m m' x e s E v res defVars DeltaMap:
eval_expr E defVars DeltaMap e v m ->
bstep s (updEnv x v E) defVars DeltaMap res m' -> (* (updDefVars (Var R x) m defVars) res m' -> *)
bstep (Let m x e s) E defVars DeltaMap res m'
|ret_b m e E v defVars DeltaMap:
eval_expr E defVars DeltaMap e v m ->
bstep (Ret e) E defVars DeltaMap v m.
(**
The free variables of a command are all used variables of exprressions
......@@ -87,14 +88,14 @@ Fixpoint liveVars V (f:cmd V) :NatSet.t :=
end.
Lemma bstep_eq_env f:
forall E1 E2 Gamma v m,
forall E1 E2 Gamma DeltaMap v m,
(forall x, E1 x = E2 x) ->
bstep f E1 Gamma v m ->
bstep f E2 Gamma v m.
bstep f E1 Gamma DeltaMap v m ->
bstep f E2 Gamma DeltaMap v m.
Proof.
induction f; intros * eq_envs bstep_E1;
inversion bstep_E1; subst; simpl in *.
- eapply eval_eq_env in H7; eauto. eapply let_b; eauto.
- eapply eval_eq_env in H8; eauto. eapply let_b; eauto.
eapply IHf. instantiate (1:=(updEnv n v0 E1)).
+ intros; unfold updEnv.
destruct (x=? n); auto.
......@@ -102,12 +103,12 @@ Proof.
- apply ret_b. eapply eval_eq_env; eauto.
Qed.
Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 :
Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 DeltaMap:
(forall n, Gamma1 n = Gamma2 n) ->
bstep f E Gamma1 vR m ->
bstep f E Gamma2 vR m.
bstep f E Gamma1 DeltaMap vR m ->
bstep f E Gamma2 DeltaMap vR m.
Proof.
revert E Gamma1 Gamma2;
revert E Gamma1 Gamma2 DeltaMap;
induction f; intros * Gamma_eq eval_f.
- inversion eval_f; subst.
econstructor; try eauto.
......@@ -118,9 +119,9 @@ Proof.
Qed.
Lemma bstep_Gamma_det f:
forall E1 E2 Gamma v1 v2 m1 m2,
bstep f E1 Gamma v1 m1 ->
bstep f E2 Gamma v2 m2 ->
forall E1 E2 Gamma DeltaMap v1 v2 m1 m2,
bstep f E1 Gamma DeltaMap v1 m1 ->
bstep f E2 Gamma DeltaMap v2 m2 ->
m1 = m2.
Proof.
induction f; intros * eval_f1 eval_f2;
......@@ -128,4 +129,4 @@ Proof.
inversion eval_f2; subst; try auto.
- eapply IHf; eauto.
- eapply Gamma_det; eauto.
Qed.
\ No newline at end of file
Qed.
......@@ -2,7 +2,7 @@ From Coq
Require Import Reals.Reals QArith.Qreals.
From Flover
Require Import ExpressionSemanticsDeterministic Environments RealRangeArith TypeValidator.
Require Import ExpressionSemantics Environments RealRangeArith TypeValidator.
Fixpoint validErrorBounds (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
(match e with
......@@ -18,23 +18,23 @@ Fixpoint validErrorBounds (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
| _ => True
end) /\
forall v__R (iv: intv) (err: error),
eval_expr_det E1 (toRTMap (toRExpMap Gamma)) (fun x m => Some 0%R) (toREval (toRExp e)) v__R REAL ->
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
FloverMap.find e A = Some (iv, err) ->
(exists v__FP m__FP,
eval_expr_det E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
(forall v__FP m__FP,
eval_expr_det E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
(Rabs (v__R - v__FP) <= (Q2R err))%R).
Lemma validErrorBounds_single e E1 E2 A Gamma DeltaMap:
validErrorBounds e E1 E2 A Gamma DeltaMap ->
forall v__R iv err,
eval_expr_det E1 (toRTMap (toRExpMap Gamma)) (fun x m => Some 0%R) (toREval (toRExp e)) v__R REAL ->
eval_expr E1 (toRTMap (toRExpMap Gamma)) (fun x m => Some 0%R) (toREval (toRExp e)) v__R REAL ->
FloverMap.find e A = Some (iv, err) ->
(exists v__FP m__FP,
eval_expr_det E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
(forall v__FP m__FP,
eval_expr_det E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
(Rabs (v__R - v__FP) <= (Q2R err))%R).
Proof.
intros validError_e;
......
This diff is collapsed.
This diff is collapsed.
......@@ -13,8 +13,8 @@ From Coq
From Flover
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Infra.RealSimps Infra.Ltacs CommandsDeterministic Environments ErrorAnalysis
ExpressionSemanticsDeterministic IntervalValidation TypeValidator
RealRangeValidator ErrorBounds ErrorValidation AffineForm AffineArithQ AffineArith.
ExpressionSemantics IntervalValidation TypeValidator RealRangeValidator
ErrorBounds ErrorValidation AffineForm AffineArithQ AffineArith.
Definition mkErrorPolyQ (err: Q) noise :=
if Qeq_bool err 0 then
......
This diff is collapsed.
......@@ -476,7 +476,7 @@ Qed.
Lemma real_eval_det_ignores_delta_map (f:expr R) (E:env) Gamma:
forall v1 DeltaMap,
eval_expr_det E (toRTMap Gamma) DeltaMap (toREval f) v1 REAL ->
eval_expr_det E (toRTMap Gamma) (fun x m => Some 0%R) (toREval f) v1 REAL.
eval_expr_det E (toRTMap Gamma) DeltaMapR (toREval f) v1 REAL.
Proof.
induction f;
intros v1 DeltaMap ev1.
......@@ -521,7 +521,7 @@ Proof.
Qed.
Theorem eval_expr_REAL_det_nondet E Gamma e v:
eval_expr_det E (toRTMap Gamma) (fun x m => Some 0%R) (toREval e) v REAL <->
eval_expr_det E (toRTMap Gamma) DeltaMapR (toREval e) v REAL <->
eval_expr E (toRTMap Gamma) (toREval e) v REAL.
Proof.
split; [eapply eval_det_eval_nondet; eauto|].
......
......@@ -1209,19 +1209,19 @@ Proof.
destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
destruct iv_e as [elo ehi].
exists (toRExpMap Gamma); intros approxE1E2.
edestruct (RoundoffErrorValidator.RoundoffErrorValidator_sound (B2Qexpr e) H0 approxE1E2 H2 eval_real R
valid_e map_e)
as [[vF [mF eval_float]] err_bounded]; auto.
assert (FloverMap.find (B2Qexpr e) Gamma = Some M64).
{ eapply typing_expr_64_bit; eauto. }
assert (M64 = mF).
{ eapply validTypes_exec; eauto. }
subst.
edestruct eval_expr_gives_IEEE; eauto.
- admit.
- intros. set_tac.
- destruct H4 as [eval_float_f eval_rel].
repeat eexists; eauto.
(* edestruct (RoundoffErrorValidator.RoundoffErrorValidator_sound (B2Qexpr e) H0 approxE1E2 H2 eval_real R *)
(* valid_e map_e) *)
(* as [[vF [mF eval_float]] err_bounded]; auto. *)
(* assert (FloverMap.find (B2Qexpr e) Gamma = Some M64). *)
(* { eapply typing_expr_64_bit; eauto. } *)
(* assert (M64 = mF). *)
(* { eapply validTypes_exec; eauto. } *)
(* subst. *)
(* edestruct eval_expr_gives_IEEE; eauto. *)
(* - admit. *)
(* - intros. set_tac. *)
(* - destruct H4 as [eval_float_f eval_rel]. *)
(* repeat eexists; eauto. *)
Admitted.
Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P
......
......@@ -144,7 +144,7 @@ Theorem validIntervalbounds_sound (f:expr Q) (A:analysisResult) (P:precond)
dVars_range_valid dVars E A ->
NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
fVars_P_sound fVars E P ->
validTypes f Gamma ->
validTypes f Gamma DeltaMapR ->
validRanges f A E (toRTMap (toRExpMap Gamma)).
Proof.
induction f;
......@@ -396,7 +396,7 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
fVars_P_sound fVars E P ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
validIntervalboundsCmd f A P dVars = true ->
validTypesCmd f Gamma ->
validTypesCmd f Gamma DeltaMapR ->
validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
Proof.
induction f;
......
......@@ -44,14 +44,14 @@ Fixpoint validRanges e (A:analysisResult) E Gamma :Prop :=
end /\
exists iv err vR,
FloverMap.find e A = Some (iv, err) /\
eval_expr E Gamma (toREval (toRExp e)) vR REAL /\
eval_expr E Gamma DeltaMapR (toREval (toRExp e)) vR REAL /\
(Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Corollary validRanges_single e A E Gamma:
validRanges e A E Gamma ->
exists iv err vR,
FloverMap.find e A = Some (iv, err) /\
eval_expr E Gamma (toREval (toRExp e)) vR REAL /\
eval_expr E Gamma DeltaMapR (toREval (toRExp e)) vR REAL /\
(Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Proof.
destruct e; intros [_ valid_e]; simpl in *; try auto.
......@@ -80,20 +80,20 @@ Fixpoint validRangesCmd (f:cmd Q) A E Gamma {struct f} : Prop :=
match f with
| Let m x e g =>
validRanges e A E Gamma /\
(forall vR, eval_expr E Gamma (toREval (toRExp e)) vR REAL ->
(forall vR, eval_expr E Gamma DeltaMapR (toREval (toRExp e)) vR REAL ->
validRangesCmd g A (updEnv x vR E) Gamma)
| Ret e => validRanges e A E Gamma
end /\
exists iv_e err_e vR,
FloverMap.find (getRetExp f) A = Some (iv_e, err_e) /\
bstep (toREvalCmd (toRCmd f)) E Gamma vR REAL /\
bstep (toREvalCmd (toRCmd f)) E Gamma DeltaMapR vR REAL /\
(Q2R (fst iv_e) <= vR <= Q2R (snd iv_e))%R.
Corollary validRangesCmd_single f A E Gamma:
validRangesCmd f A E Gamma ->
exists iv_e err_e vR,
FloverMap.find (getRetExp f) A = Some (iv_e, err_e) /\
bstep (toREvalCmd (toRCmd f)) E Gamma vR REAL /\
bstep (toREvalCmd (toRCmd f)) E Gamma DeltaMapR vR REAL /\
(Q2R (fst iv_e) <= vR <= Q2R (snd iv_e))%R.
Proof.
destruct f; simpl in *; intros [ _ valid_f]; auto.
......@@ -284,7 +284,8 @@ Proof.
rewrite N.eqb_refl in *; congruence.
Qed.
Lemma validRanges_ssa_extension (e: expr Q) (e' : expr Q) A E Gamma vR' m n c fVars dVars outVars:
Lemma validRanges_ssa_extension (e: expr Q) (e' : expr Q) A E Gamma
vR' m n c fVars dVars outVars:
ssa (Let m n e' c) (fVars dVars) outVars ->
NatSet.Subset (usedVars e) (fVars dVars) ->
~ (n fVars dVars) ->
......@@ -364,4 +365,4 @@ Proof.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption. *)
rewrite usedVars_toREval_toRExp_compat; auto.
Qed.
\ No newline at end of file
Qed.
......@@ -25,7 +25,7 @@ Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : precond) dVa
RangeValidator e A P dVars = true ->
dVars_range_valid dVars E A ->
affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
validTypes e Gamma ->
validTypes e Gamma DeltaMapR ->
fVars_P_sound (usedVars e) E P ->
validRanges e A E (toRTMap (toRExpMap Gamma)).
Proof.
......@@ -76,7 +76,7 @@ Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond) d
affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
fVars_P_sound fVars E P ->
NatSet.Subset (freeVars f -- dVars) fVars ->
validTypesCmd f Gamma ->
validTypesCmd f Gamma DeltaMapR ->
validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
Proof.
intros ranges_valid; intros.
......@@ -104,4 +104,4 @@ Proof.
exprAfs noise iexpmap inoise imap
Hchecked Hinoise Himap Hafcheck H H1 H3 HfVars)
as [map2 [af [vR [aiv [aerr sound_affine]]]]]; intuition.
Qed.
\ No newline at end of file
Qed.
......@@ -34,8 +34,7 @@ Proof.
unfold RoundoffErrorValidator.
intros; cbn in *.
destruct (validErrorbound e Gamma A dVars) eqn: Hivvalid.
- admit.
(* eapply validErrorbound_sound; eauto. *)
- eapply validErrorbound_sound; eauto.
- destruct (validErrorboundAA e Gamma A dVars 1 (FloverMap.empty (affine_form Q))) eqn: Hafvalid;
[|congruence].
destruct p as (expr_map, noise).
......@@ -59,7 +58,7 @@ Proof.
[now rewrite FloverMapFacts.P.F.empty_in_iff|].
split; eauto.
eapply Hall; eauto; now rewrite FloverMapFacts.P.F.empty_in_iff.
Admitted.
Qed.
Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType)
(A:analysisResult) (dVars:NatSet.t) :=
......@@ -92,4 +91,4 @@ Proof.
split.
- eapply validErrorboundCmd_gives_eval; eauto.
- intros. eapply validErrorboundCmd_sound; eauto.
Admitted.
Qed.
This diff is collapsed.
......@@ -178,10 +178,10 @@ Proof.
+ hnf; intros; split; auto.
Qed.
Lemma ssa_shadowing_free m x y v v' e f inVars outVars E defVars:
Lemma ssa_shadowing_free m x y v v' e f inVars outVars E defVars DeltaMap:
ssa (Let m x (toREval (toRExp e)) (toREvalCmd (toRCmd f))) inVars outVars ->
NatSet.In y inVars ->
eval_expr E defVars (toREval (toRExp e)) v REAL ->
eval_expr E defVars DeltaMap (toREval (toRExp e)) v REAL ->
forall E n, updEnv x v (updEnv y v' E) n = updEnv y v' (updEnv x v E) n.
Proof.
intros ssa_let y_free eval_e.
......@@ -210,12 +210,13 @@ Proof.
set_tac.
Qed.
Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma vR vR' m n c fVars dVars outVars:
Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma DeltaMap
vR vR' m n c fVars dVars outVars:
ssa (Let m n e' c) (fVars dVars) outVars ->
NatSet.Subset (usedVars e) (fVars dVars) ->
~ (n fVars dVars) ->
eval_expr E Gamma e vR REAL ->
eval_expr (updEnv n vR' E) Gamma e vR REAL.
eval_expr E Gamma DeltaMap e vR REAL ->
eval_expr (updEnv n vR' E) Gamma DeltaMap e vR REAL.
Proof.
intros Hssa Hsub Hnotin Heval.
eapply eval_expr_ignore_bind; [auto |].
......
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