Commit 35edd282 authored by Nikita Zyuzin's avatar Nikita Zyuzin

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

parents 8804c37e 0a61d6ec
......@@ -3,7 +3,7 @@ Require Import Recdef.
Require Import Flover.AffineForm Flover.AffineArithQ Flover.AffineArith.
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Require Import Flover.Infra.Ltacs Flover.Infra.RealSimps Flover.Typing Flover.ssaPrgs.
Require Import Flover.IntervalValidation.
Require Import Flover.IntervalValidation Flover.RealRangeArith.
Lemma usedVars_eq_compat e1 e2:
Q_orderedExps.eq e1 e2 ->
......@@ -277,7 +277,7 @@ Fixpoint validAffineBounds (e: expr Q) (A: analysisResult) (P: precond) (validVa
olet valid := validAffineBounds e' A P validVars exprsAf currentMaxNoise in
let (exprsAf', n') := valid in
olet af := FloverMap.find e' exprsAf' in
match o with
match o with
| Neg =>
updateExpMap e (AffineArithQ.negate_aff af) n' exprsAf' intv
| Inv =>
......@@ -321,7 +321,7 @@ Fixpoint validAffineBounds (e: expr Q) (A: analysisResult) (P: precond) (validVa
let (exprsAf3, n3) := valid3 in
olet af3 := FloverMap.find e3 exprsAf3 in
updateExpMapSucc e (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 n3)) n3 exprsAf3 intv
| Downcast _ e' =>
| Downcast _ e' =>
olet valid' := validAffineBounds e' A P validVars exprsAf currentMaxNoise in
let (exprsAf', n') := valid' in
olet asubres := FloverMap.find e' A in
......@@ -651,7 +651,7 @@ Qed.
Lemma afQ2R_fresh n a:
fresh n a <-> fresh n (afQ2R a).
Proof.
split; induction a; intros *.
split; induction a; intros *.
all: try (unfold fresh, get_max_index; rewrite get_max_index_aux_equation; now simpl).
all: intros A.
all: remember A as A' eqn:tmp; clear tmp.
......@@ -728,7 +728,7 @@ Definition affine_fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop :=
NatSet.In v fVars ->
exists vR, E v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R.
Definition affine_vars_typed (S: NatSet.t) (Gamma: nat -> option mType) :=
forall v, NatSet.In v S ->
exists m: mType, Gamma v = Some m.
......@@ -814,7 +814,7 @@ Proof.
Qed.
Lemma validAffineBounds_sound (e: expr Q) (A: analysisResult) (P: precond)
fVars dVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
fVars dVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
(forall e, (exists af, FloverMap.find e iexpmap = Some af) ->
checked_expressions A E Gamma fVars dVars e iexpmap inoise map1) ->
(inoise > 0)%nat ->
......@@ -2165,7 +2165,7 @@ Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (valid
end.
Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond)
fVars dVars outVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
fVars dVars outVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
(forall e, (exists af, FloverMap.find e iexpmap = Some af) ->
checked_expressions A E Gamma fVars dVars e iexpmap inoise map1) ->
(inoise > 0)%nat ->
......
......@@ -4,12 +4,12 @@
Running this function on the encoded analysis result gives the desired theorem
as shown in the soundness theorem.
**)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Flover.Infra.RealSimps Flover.Infra.RationalSimps Flover.Infra.RealRationalProps Flover.Infra.Ltacs.
Require Import Flover.RealRangeValidator Flover.RoundoffErrorValidator Flover.Environments Flover.Typing Flover.FPRangeValidator.
From Flover
Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
Environments Typing FPRangeValidator ExpressionAbbrevs Commands.
Require Export Coq.QArith.QArith.
Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.
Require Export Infra.ExpressionAbbrevs Flover.Commands.
(** Certificate checking function **)
Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
......@@ -68,10 +68,13 @@ Proof.
{ unfold vars_typed. intros; apply types_defined. set_tac. destruct H1; set_tac.
split; try auto. hnf; intros; set_tac. }
rename R into validFPRanges.
edestruct (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=defVars) (E:=E1))
as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]]; eauto.
assert (validRanges e absenv E1 defVars) as valid_e.
{ eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=defVars) (E:=E1));
auto. }
pose proof (validRanges_single _ _ _ _ valid_e) as valid_single;
destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
destruct iv_e as [elo ehi].
edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType)) L approxE1E2 H0 eval_real R0 L1 H P_valid H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType)) L approxE1E2 H0 eval_real R0 valid_e H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
exists (elo, ehi), err_e, vR, vF, mF; split; auto.
Qed.
......@@ -81,7 +84,7 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) d
then
if (RangeValidatorCmd f absenv P NatSet.empty) &&
FPRangeValidatorCmd f absenv tMap NatSet.empty
then (validErrorboundCmd f tMap absenv NatSet.empty)
then (RoundoffErrorValidatorCmd f tMap absenv NatSet.empty)
else false
else false.
......@@ -126,12 +129,13 @@ Proof.
destruct H0; set_tac. }
assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
as freeVars_contained by set_tac.
edestruct (validIntervalboundsCmd_sound)
as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]]; eauto.
assert (validRangesCmd f absenv E1 defVars) as valid_f.
{ eapply RangeValidatorCmd_sound; eauto.
unfold affine_dVars_range_valid; intros.
set_tac. }
pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
destruct iv as [f_lo f_hi].
edestruct validErrorboundCmd_gives_eval as [vF [mF eval_float]]; eauto.
edestruct (RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto.
exists (f_lo, f_hi), err, vR, vF, mF; split; try auto.
split; try auto; split; try auto.
intros.
eapply validErrorboundCmd_sound; eauto.
Qed.
......@@ -2181,7 +2181,7 @@ Theorem validErrorboundCmd_gives_eval (f:cmd Q) :
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL ->
validErrorboundCmd f Gamma A dVars = true ->
validRangesCmd f A E1 (toRMap defVars) ->
validRangesCmd f A E1 defVars ->
vars_typed (NatSet.union fVars dVars) defVars ->
FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
(exists vF m,
......@@ -2241,32 +2241,12 @@ Proof.
split; try auto. }
{ eapply swap_Gamma_bstep with (Gamma1 := updDefVars n REAL (toRMap defVars));
eauto using Rmap_updVars_comm. }
{ eapply valid_cont.
{ intros v1 v1_mem.
unfold updEnv.
case_eq (v1 =? n); intros v1_eq.
- apply Nat.eqb_eq in v1_eq; subst.
exists v, (q1, q2), e1; split; try auto; split; try auto; simpl.
destruct (validIntervalbounds_sound e (E:=E1) (Gamma:=defVars) L (fVars:=fVars))
as [iv_e' [ err_e' [vR_e [map_e [eval_real_e bounded_real_e]]]]];
eauto.
rewrite map_e in *; inversion Heqo; subst.
pose proof (meps_0_deterministic _ eval_real_e H7); subst.
simpl in *. inversion Heqo0; subst; lra.
- rewrite Nat.eqb_neq in v1_eq; set_tac.
destruct v1_mem; subst; try congruence.
apply fVars_sound ; try auto.
destruct H0; auto. }
{ intros v1 mem_fVars.
specialize (P_valid v1 mem_fVars).
unfold updEnv.
case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try auto.
rewrite Nat.eqb_eq in case_v1; subst.
assert (NatSet.In n (NatSet.union fVars dVars))
as in_union
by (rewrite NatSet.union_spec; auto).
rewrite <- NatSet.mem_spec in in_union.
rewrite in_union in *; congruence. }
{ apply validRangesCmd_swap with (Gamma1 := updDefVars n REAL defVars).
- intros x.
unfold toRMap, updDefVars.
destruct (x =? n) eqn:?; auto.
- apply valid_cont.
apply swap_Gamma_eval_expr with (Gamma1 := toRMap defVars); try auto. }
{ intros v1 v1_mem; set_tac.
unfold updDefVars.
case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try eauto.
......@@ -2277,16 +2257,17 @@ Proof.
rewrite Nat.eqb_neq in case_v1; congruence. }
{ exists vF_res; exists m_res; try auto.
econstructor; eauto. }
+ destruct valid_intv as [[? ?] ?]; auto.
- inversion eval_real; subst.
unfold updEnv; simpl.
unfold validErrorboundCmd in valid_bounds.
simpl in *.
destruct valid_intv.
edestruct validErrorbound_sound as [[vF [mF eval_e]] bounded_e]; eauto.
exists vF; exists mF; econstructor; eauto.
Qed.
Theorem validErrorboundCmd_sound (f:cmd Q):
forall A E1 E2 outVars fVars dVars vR vF mF elo ehi err P Gamma defVars,
forall A E1 E2 outVars fVars dVars vR vF mF elo ehi err Gamma defVars,
typeCheckCmd f defVars Gamma = true ->
approxEnv E1 defVars A fVars dVars E2 ->
ssa f (NatSet.union fVars dVars) outVars ->
......@@ -2294,16 +2275,14 @@ Theorem validErrorboundCmd_sound (f:cmd Q):
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL ->
bstep (toRCmd f) E2 defVars vF mF ->
validErrorboundCmd f Gamma A dVars = true ->
validIntervalboundsCmd f A P dVars = true ->
dVars_range_valid dVars E1 A ->
fVars_P_sound fVars E1 P ->
validRangesCmd f A E1 defVars ->
vars_typed (NatSet.union fVars dVars) defVars ->
FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
(Rabs (vR - vF) <= (Q2R err))%R.
Proof.
induction f;
intros * type_f approxc1c2 ssa_f freeVars_subset eval_real eval_float
valid_bounds valid_intv fVars_sound P_valid types_defined A_res;
valid_bounds valid_intv types_defined A_res;
cbn in *; Flover_compute; try congruence; type_conv; subst.
- inversion eval_real;
inversion eval_float;
......@@ -2317,25 +2296,20 @@ Proof.
match goal with
| [H : validErrorbound _ _ _ _ = true |- _] =>
eapply validErrorbound_sound
with (err := e2) (elo := fst(i)) (ehi:= snd(i)) in H; edestruct i; eauto;
with (err := e0) (elo := fst(i)) (ehi:= snd(i)) in H; edestruct i; eauto;
destruct H as [[vFe [mFe eval_float_e]] bounded_e]
end.
canonize_hyps.
rename R into valid_rec.
rewrite (typingSoundnessExp _ _ L0 eval_float_e) in *;
rewrite (typingSoundnessExp _ _ L eval_float_e) in *;
simpl in *.
(* destruct (Gamma (Var Q n)); try congruence. *)
(* match goal with *)
(* | [ H: _ && _ = true |- _] => andb_to_prop H *)
(* end. *)
(* type_conv. *)
apply (IHf A (updEnv n v E1) (updEnv n v0 E2) outVars fVars
(NatSet.add n dVars) vR vF mF elo ehi err P Gamma
(NatSet.add n dVars) vR vF mF elo ehi err Gamma
(updDefVars n m1 defVars));
eauto.
+ eapply approxUpdBound; try eauto.
simpl in *.
apply Rle_trans with (r2:= Q2R e2); try lra.
apply Rle_trans with (r2:= Q2R e0); try lra.
eapply bounded_e; eauto.
+ eapply ssa_equal_set; eauto.
hnf. intros a; split; intros in_set.
......@@ -2354,34 +2328,13 @@ Proof.
split; try auto.
+ eapply swap_Gamma_bstep with (Gamma1 := updDefVars n REAL (toRMap defVars));
eauto using Rmap_updVars_comm.
+ intros v1 v1_mem.
unfold updEnv.
case_eq (v1 =? n); intros v1_eq.
* apply Nat.eqb_eq in v1_eq; subst.
exists v, (q1,q2), e1; split; try auto; split; try auto.
simpl. rewrite <- R1, <- R0.
destruct (validIntervalbounds_sound e L (E:=E1) (Gamma:=defVars) (fVars:=fVars))
as [iv_e [ err_e [ vR_e [ map_e [eval_real_e bounded_real_e]]]]];
eauto.
repeat destr_factorize.
pose proof (meps_0_deterministic _ eval_real_e H7); subst.
inversion Heqo0; subst.
simpl in *; auto.
* rewrite Nat.eqb_neq in v1_eq.
set_tac.
destruct v1_mem as [? | [? ?]].
{ exfalso; apply v1_eq; auto. }
{ apply fVars_sound ; auto. }
+ intros v1 mem_fVars.
specialize (P_valid v1 mem_fVars).
unfold updEnv.
case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try auto.
rewrite Nat.eqb_eq in case_v1; subst.
assert (NatSet.In n (NatSet.union fVars dVars))
as in_union
by (rewrite NatSet.union_spec; auto).
rewrite <- NatSet.mem_spec in in_union.
rewrite in_union in *; congruence.
+ apply validRangesCmd_swap with (Gamma1 := updDefVars n REAL defVars).
* intros x.
unfold toRMap, updDefVars.
destruct (x =? n) eqn:?; auto.
* destruct valid_intv as [[? valid_cont] ?].
apply valid_cont.
apply swap_Gamma_eval_expr with (Gamma1 := toRMap defVars); try auto.
+ intros v1 v1_mem; set_tac.
unfold updDefVars.
case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try eauto.
......@@ -2390,10 +2343,11 @@ Proof.
destruct v1_mem as [v_fVar | v_dVar]; try auto.
rewrite NatSet.add_spec in v_dVar. destruct v_dVar; try auto.
subst; rewrite Nat.eqb_refl in case_v1; congruence.
+ destruct valid_intv as [[? ?] ?]; auto.
- inversion eval_real; subst.
inversion eval_float; subst.
unfold updEnv; simpl.
unfold validErrorboundCmd in valid_bounds.
simpl in *.
destruct valid_intv as [? ?].
edestruct validErrorbound_sound as [[* [* eval_e]] bounded_e]; eauto.
Qed.
......@@ -231,24 +231,24 @@ Definition checked_error_expressions (A: analysisResult) (E1 E2:env) Gamma e
let mAbs := maxAbs (toIntv af) in
(Rabs (vR - vF) <= (Q2R mAbs))%R.
Theorem validErrorboundAA_sound e:
forall E1 E2 P Gamma defVars nR A elo ehi tMap fVars dVars currNoise maxNoise initMap resMap M1,
(forall e vR,
FloverMap.In e initMap ->
checked_error_expressions A E1 E2 Gamma e initMap currNoise M1 vR) ->
approxEnv E1 defVars A fVars dVars E2 ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
affine_dVars_range_valid dVars E1 A currNoise initMap M1 ->
affine_fVars_P_sound fVars E1 P ->
affine_vars_typed fVars Gamma ->
validErrorboundAA e Gamma A tMap currNoise initMap = Some (resMap, maxNoise) ->
RangeValidator e A P dVars = true ->
typeCheck e defVars Gamma = true ->
vars_typed (NatSet.union fVars dVars) defVars ->
FloverMap.find e A = Some ((elo,ehi),err) ->
(exists nF m,
eval_expr E2 defVars (toRExp e) nF m) /\
(forall nF m,
eval_expr E2 defVars (toRExp e) nF m ->
(Rabs (nR - nF) <= (Q2R err))%R).
(* Theorem validErrorboundAA_sound e: *)
(* forall E1 E2 P Gamma defVars nR A elo ehi tMap fVars dVars currNoise maxNoise initMap resMap M1, *)
(* (forall e vR, *)
(* FloverMap.In e initMap -> *)
(* checked_error_expressions A E1 E2 Gamma e initMap currNoise M1 vR) -> *)
(* approxEnv E1 defVars A fVars dVars E2 -> *)
(* NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars -> *)
(* eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL -> *)
(* affine_dVars_range_valid dVars E1 A currNoise initMap M1 -> *)
(* affine_fVars_P_sound fVars E1 P -> *)
(* affine_vars_typed fVars Gamma -> *)
(* validErrorboundAA e Gamma A tMap currNoise initMap = Some (resMap, maxNoise) -> *)
(* RangeValidator e A P dVars = true -> *)
(* typeCheck e defVars Gamma = true -> *)
(* vars_typed (NatSet.union fVars dVars) defVars -> *)
(* FloverMap.find e A = Some ((elo,ehi),err) -> *)
(* (exists nF m, *)
(* eval_expr E2 defVars (toRExp e) nF m) /\ *)
(* (forall nF m, *)
(* eval_expr E2 defVars (toRExp e) nF m -> *)
(* (Rabs (nR - nF) <= (Q2R err))%R). *)
This diff is collapsed.
This diff is collapsed.
......@@ -14,7 +14,7 @@ Module OWL.
Proof.
now unfold eq; split; subst.
Qed.
Definition compare := Compare_dec.nat_compare.
Definition compare := Nat.compare.
Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
Proof.
......@@ -42,8 +42,6 @@ Notation "x 'mem' S" := (NatSet.mem x S) (at level 0, no associativity).
Notation "x '∈' S" := (NatSet.In x S) (at level 100, no associativity).
Check (forall x S, x S -- {{x}}).
Lemma not_in_not_mem:
forall n S,
NatSet.mem n S = false ->
......
......@@ -91,7 +91,6 @@ Proof.
eapply swap_Gamma_eval_expr; eauto.
Qed.
Lemma validRanges_swap Gamma1 Gamma2:
forall e A E,
(forall n, (toRMap Gamma1) n = toRMap (Gamma2) n) ->
......@@ -107,9 +106,9 @@ Proof.
lra]).
- destruct valid1; auto.
- destruct valid1 as [[? [? ?]] ?]; auto.
- admit.
- destruct valid1 as [[? [? ?]] ?]; auto.
- destruct valid1; auto.
Admitted.
Qed.
Fixpoint validRangesCmd (f:cmd Q) A E Gamma {struct f} : Prop :=
match f with
......@@ -133,3 +132,26 @@ Corollary validRangesCmd_single f A E Gamma:
Proof.
destruct f; simpl in *; intros [ _ valid_f]; auto.
Qed.
Lemma validRangesCmd_swap:
forall f A E Gamma1 Gamma2,
(forall n, (toRMap Gamma1) n = toRMap (Gamma2) n) ->
validRangesCmd f A E Gamma1 ->
validRangesCmd f A E Gamma2.
Proof.
induction f; intros * Gamma_swap valid1; simpl in *; try (split; auto);
try (
destruct valid1 as [_ [? [? [? [? [? ?]]]]]];
repeat eexists; eauto;
[eapply swap_Gamma_bstep with (Gamma1 := (toRMap Gamma1)); eauto |
lra |
lra]).
- destruct valid1 as [[? valid_all_exec] ?]; split.
+ eapply validRanges_swap; eauto.
+ intros. eapply IHf; [ | eapply valid_all_exec].
* intros x. unfold updDefVars.
destruct (x =? n) eqn:?; auto.
* eapply swap_Gamma_eval_expr with (Gamma1 := toRMap Gamma2); eauto.
- destruct valid1.
eapply validRanges_swap; eauto.
Qed.
\ No newline at end of file
......@@ -2,7 +2,8 @@ From Coq
Require Import Reals.Reals QArith.Qreals.
From Flover
Require Export Infra.ExpressionAbbrevs ErrorValidation RealRangeValidator.
Require Export Infra.ExpressionAbbrevs ErrorValidation RealRangeValidator
Typing Environments.
Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType) (A:analysisResult) (dVars:NatSet.t) :=
(* if *)
......@@ -12,17 +13,15 @@ Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType) (A:analysi
Theorem RoundoffErrorValidator_sound:
forall (e : expr Q) (E1 E2 : env) (fVars dVars : NatSet.t) (A : analysisResult)
(nR : R) (err : error) (P : precond) (elo ehi : Q) (Gamma : FloverMap.t mType)
(nR : R) (err : error) (elo ehi : Q) (Gamma : FloverMap.t mType)
(defVars : nat -> option mType),
Typing.typeCheck e defVars Gamma = true ->
Environments.approxEnv E1 defVars A fVars dVars E2 ->
typeCheck e defVars Gamma = true ->
approxEnv E1 defVars A fVars dVars E2 ->
NatSet.Subset (usedVars e -- dVars) fVars ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
RoundoffErrorValidator e Gamma A dVars = true ->
RangeValidator e A P dVars = true ->
IntervalValidation.dVars_range_valid dVars E1 A ->
IntervalValidation.fVars_P_sound fVars E1 P ->
IntervalValidation.vars_typed (fVars dVars) defVars ->
validRanges e A E1 defVars ->
vars_typed (fVars dVars) defVars ->
FloverMap.find (elt:=intv * error) e A = Some (elo, ehi, err) ->
(exists (nF : R) (m : mType), eval_expr E2 defVars (toRExp e) nF m) /\
(forall (nF : R) (m : mType), eval_expr E2 defVars (toRExp e) nF m -> (Rabs (nR - nF) <= Q2R err)%R).
......@@ -30,3 +29,33 @@ Proof.
intros. cbn in *.
eapply validErrorbound_sound; eauto.
Qed.
Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType) (A:analysisResult) (dVars:NatSet.t) :=
(* if *)
validErrorboundCmd f tMap A dVars.
(*then true *)
(* else validAffineErrorboundsCmd e A tMap dVars ... *)
Theorem RoundoffErrorValidatorCmd_sound f:
forall A E1 E2 outVars fVars dVars vR elo ehi err Gamma defVars,
typeCheckCmd f defVars Gamma = true ->
approxEnv E1 defVars A fVars dVars E2 ->
ssa f (NatSet.union fVars dVars) outVars ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL ->
validErrorboundCmd f Gamma A dVars = true ->
validRangesCmd f A E1 defVars ->
vars_typed (NatSet.union fVars dVars) defVars ->
FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
(exists vF m,
bstep (toRCmd f) E2 defVars vF m) /\
(forall vF mF,
bstep (toRCmd f) E2 defVars vF mF ->
(Rabs (vR - vF) <= (Q2R err))%R).
Proof.
intros.
cbn in *.
split.
- eapply validErrorboundCmd_gives_eval; eauto.
- intros. eapply validErrorboundCmd_sound; eauto.
Qed.
\ No newline at end of file
#bytes:
# ocamlc -c CoqChecker.ml
# ocamlc -o coq_checker_bytes nums.cma big.ml CoqChecker.ml coq_main.ml
native:
ocamlc -c big.ml
ocamlc -c CoqChecker.ml
ocamlc -c CoqChecker.mli
ocamlc -o coq_checker_native nums.cma big.ml CoqChecker.ml coq_main.ml
all: native
Require Import Coq.Strings.Ascii Coq.Strings.String Coq.Lists.List Coq.Reals.Reals.
Require Import Coq.Strings.Ascii Coq.Strings.String Coq.Lists.List
Coq.Reals.Reals Coq.Bool.Bool Coq.QArith.QArith.
Require Import CertificateChecker Infra.MachineType.
......
Subproject commit c25dae0a1ede617a25e49162f6f47ac9a1a2381a
Subproject commit b801379405021120d0dd2b8d3a3a886c84a114a4
#!/bin/bash
###############################################################################
# #
# Affine Arithmetic Experiments for FMCAD 2018 paper #
# First run Daisy on all files found in the folder given as third argument #
# certificates and log roundoff errors in a csv file. #
# Then benchmark each of the FloVer implementations by measuring runtime #
# when checking the generated certificate. #
# #
###############################################################################
arr=()
while IFS= read -r -d $'\0'; do
arr+=("$REPLY")
# FIXME: Use a proper directory or a parameter?
done < <(find $3 -name "*.scala" -print0)
DATE=`date +%H%M%d%m%y`
mkdir /tmp/artifact_affine_$DATE
for file in "${arr[@]}"
do
#Get the filename
FILEPATH=${file/daisy\//.\/}
FILE=${file/*\//}
FILENAME=${FILE/.scala/}
PMAP=${FILE/scala/txt}
CERTNAME="certificate_$FILENAME"
# Generate a certificate with Daisy
echo -n $FILENAME >>$1
cd ./daisy
if [ ! -f testcases/mixed-precision-maps/$PMAP ];
then
echo "Doing single precision eval for $FILENAME" >>$2
RESULT=$( { /usr/bin/time -f ", %e" \
./daisy $FILEPATH --certificate=coq \
--rangeMethod=affine \
--errorMethod=interval \
--results-csv=$FILENAME \
>>$2 \
; } 2>&1 )
echo -n $RESULT >> $1
else
echo "Doing mixed-precision eval for $FILENAME" >>$2
RESULT=$( { /usr/bin/time -f ", %e" \
./daisy $FILEPATH --certificate=coq \
--rangeMethod=affine \
--errorMethod=interval \
--mixed-precision=testcases/mixed-precision-maps/$PMAP \
--results-csv=$FILENAME \
>>$2 \
; } 2>&1)
echo -n $RESULT >> $1
fi
mv ./output/$FILENAME.csv /tmp/artifact_$DATE
cd ..
#run coq checker
echo "Working on Coq $CERTNAME" >>$2
RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
./daisy/output/$CERTNAME.v; } 2>&1)
echo $RESULT >>$1
mv ./daisy/output/certificate_* /tmp/artifact_affine_$DATE/
done
#!/bin/bash
##############################################################################
# #
# Interval Arithmetic Experiments for FMCAD 2018 paper #
# First run Daisy on all files found in the folder given as third argument #
# certificates and log roundoff errors in a csv file. #
# Then benchmark each of the FloVer implementations by measuring runtime #
# when checking the generated certificate. #
# #
##############################################################################
PROVERS=(coq hol4 binary)
arr=()
while IFS= read -r -d $'\0'; do
arr+=("$REPLY")
# FIXME: Use a proper directory or a parameter?
done < <(find $3 -name "*.scala" -print0)
DATE=`date +%H%M%d%m%y`
mkdir /tmp/artifact_$DATE
echo "Creating HOL4 heap for evaluation" >>$2
cd ./hol4/output/
Holmake heap >>$2
cd ../../
for file in "${arr[@]}"